src/ZF/Tools/induct_tacs.ML

   val name = "ZF/datatypes";
   type T = datatype_info Symtab.table;
 
   val empty = Symtab.empty;
   val copy = I;
-  val finish = I;
   val prep_ext = I;
   val merge: T * T -> T = Symtab.merge (K true);
 
   fun print sg tab =
     Pretty.writeln (Pretty.strs ("datatypes:" ::

   val name = "ZF/constructors"
   type T = constructor_info Symtab.table
 
   val empty = Symtab.empty
   val copy = I;
-  val finish = I;
   val prep_ext = I
   val merge: T * T -> T = Symtab.merge (K true)
 
   fun print sg tab = ()   (*nothing extra to print*)
 end;