# HG changeset patch
# User wenzelm
# Date 924266997 -7200
# Node ID 268aa3c4a059ffce943646d0f9af90d297f090a1
# Parent  7c59a55bae941fafd85249da4403a59e22e43bb7
print_datatypes;

diff -r 7c59a55bae94 -r 268aa3c4a059 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 **)