HOL makes bad Theories with certain Hol_datatype-defined constructor names

[SOwens]

At the least, the name "Success" leads HOL to be unable to load the theory.

milo:tmp so294$ cat testScript.sml
open bossLib Theory;

val _ = new_theory "test";

val _ = Hol_datatype t = Success;

val _ = export_theory ();
milo:tmp so294$ holmake testTheory.uo
Analysing testScript.sml
Linking testScript.uo to produce theory-builder executable
Poly/ML 5.4.1 Release

<<HOL message: Created theory "test">>
Saved theorem _____ "num2t_t2num"
Saved theorem _____ "t2num_num2t"
Saved theorem _____ "num2t_11"
Saved theorem _____ "t2num_11"
Saved theorem _____ "num2t_ONTO"
Saved theorem _____ "t2num_ONTO"
Saved theorem _____ "num2t_thm"
Saved theorem _____ "t2num_thm"
Saved theorem _____ "t_EQ_t"
Saved theorem _____ "t_case_def"
Saved theorem _____ "datatype_t"
Saved theorem _____ "t_case_cong"
Saved theorem _____ "t_nchotomy"
Saved theorem _____ "t_Axiom"
Saved theorem _____ "t_induction"
<<HOL message: Defined type: "t">>
Exporting theory "test" ... done.
Theory "test" took 0.003s to build
Analysing testTheory.sml
Analysing testTheory.sig
milo:tmp so294$ hol

---

   HOL-4 [Kananaskis 8 (stdknl, built Tue Jul 31 12:53:57 2012)]

   For introductory HOL help, type: help "hol";

---

[Use-ing configuration file /Users/so294/.hol-config.sml]
Poly/ML 5.4.1 Release

load "testTheory";
Error- in '.HOLMK/testTheory.sml', line 69.
Constructor must be applied to an argument pattern. Found near Success
Error- in '.HOLMK/testTheory.sml', line 111.
Elements in a list have different types.
Items 1-2: ("t_TY_DEF", t_TY_DEF, DB.Def), ("t_BIJ", t_BIJ, DB.Def) :
string * thm * class
Item 3: ("Success", Success, DB.Def) :
string * (string -> runresult) * class
Reason: Can't unify thm to string -> runresult (Incompatible types)
Found near
[
("t_TY_DEF", t_TY_DEF, DB.Def),
("t_BIJ", t_BIJ, DB.Def),
("Success", Success, ...),
("t_size_def", ...),
(...),
...
]
Error- in '.HOLMK/testTheory.sml', line 1.
Structure does not match signature.
Signature: val Success: thm
Structure: Not present
Found near
struct
val
_ =
if ! Globals.print_thy_loads then print "Loading testTheory ... "
else ()
open Type Term Thm
infixr 0 -->
fun ...
fun ...
...
...
end
Exception- Fail "Static Errors" raised