print_datatypes;
authorwenzelm
Fri, 16 Apr 1999 14:49:57 +0200
changeset 6441 268aa3c4a059
parent 6440 7c59a55bae94
child 6442 6a95ceaa977e
print_datatypes;
src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Fri Apr 16 14:49:34 1999 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Fri Apr 16 14:49:57 1999 +0200
@@ -62,6 +62,7 @@
        size : thm list,
        simps : thm list}
   val get_datatypes : theory -> DatatypeAux.datatype_info Symtab.table
+  val print_datatypes : theory -> unit
   val datatype_info_sg : Sign.sg -> string -> DatatypeAux.datatype_info
   val datatype_info : theory -> string -> DatatypeAux.datatype_info
   val constrs_of : theory -> string -> term list option
@@ -97,6 +98,7 @@
 val get_datatypes_sg = DatatypesData.get_sg;
 val get_datatypes = DatatypesData.get;
 val put_datatypes = DatatypesData.put;
+val print_datatypes = DatatypesData.print;
 
 
 (** theory information about datatypes **)