datatype_thm_to_string
EmitTeX.datatype_thm_to_string : thm -> string
Converts a datatype theorem to a string.
An invocation of datatype_thm_to_string thm, where thm is a datatype
theorem produced by Hol_datatype, will return a string that
corresponds with the orginal datatype declaration.
Failure
Will fail if the supplied theorem is not a datatype theorem, as created
by Hol_datatype.
Example
> new_theory "example";
<<HOL message: Restarting theory "example">>
<<HOL warning: Theory.callhooks: Hook Parse.clear_consts_from_grammar failed on event NewTheory{oldseg = "example", newseg = "example"} with problem
Exception raised at Term.dest_thy_const: not a const
>>
val it = (): unit
> val _ = Hol_datatype `example = First | Second`;
<<HOL message: Defined type: "example">>
> EmitTeX.datatype_thm_to_string (theorem "datatype_example");
val it = "example = First | Second": string