src/ZF/Tools/induct_tacs.ML

--- a/src/ZF/Tools/induct_tacs.ML	Sun May 06 21:50:17 2007 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Mon May 07 00:49:59 2007 +0200
@@ -31,19 +31,14 @@
    exhaustion : thm};
 
 structure DatatypesData = TheoryDataFun
-(struct
-  val name = "ZF/datatypes";
+(
   type T = datatype_info Symtab.table;
-
   val empty = Symtab.empty;
   val copy = I;
   val extend = I;
   fun merge _ tabs : T = Symtab.merge (K true) tabs;
+);
 
-  fun print thy tab =
-    Pretty.writeln (Pretty.strs ("datatypes:" ::
-      map #1 (NameSpace.extern_table (Sign.type_space thy, tab))));
-end);
 
 
 (** Constructor information: needed to map constructors to datatypes **)
@@ -56,15 +51,13 @@
 
 
 structure ConstructorsData = TheoryDataFun
-(struct
-  val name = "ZF/constructors"
+(
   type T = constructor_info Symtab.table
   val empty = Symtab.empty
   val copy = I;
   val extend = I
   fun merge _ tabs: T = Symtab.merge (K true) tabs;
-  fun print _ _= ();
-end);
+);
 
 structure DatatypeTactics : DATATYPE_TACTICS =
 struct
@@ -185,13 +178,11 @@
 (* theory setup *)
 
 val setup =
- (DatatypesData.init #>
-  ConstructorsData.init #>
   Method.add_methods
     [("induct_tac", Method.goal_args Args.name induct_tac,
       "induct_tac emulation (dynamic instantiation!)"),
      ("case_tac", Method.goal_args Args.name exhaust_tac,
-      "datatype case_tac emulation (dynamic instantiation!)")]);
+      "datatype case_tac emulation (dynamic instantiation!)")];
 
 
 (* outer syntax *)