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">>
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