src/ZF/Tools/induct_tacs.ML

--- a/src/ZF/Tools/induct_tacs.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/ZF/Tools/induct_tacs.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -29,13 +29,12 @@
    mutual_induct : thm,
    exhaustion : thm};
 
-structure DatatypesData = TheoryDataFun
+structure DatatypesData = Theory_Data
 (
   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 merge data : T = Symtab.merge (K true) data;
 );
 
 
@@ -49,13 +48,12 @@
    rec_rewrites : thm list};  (*recursor equations*)
 
 
-structure ConstructorsData = TheoryDataFun
+structure ConstructorsData = Theory_Data
 (
   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 merge data = Symtab.merge (K true) data;
 );
 
 structure DatatypeTactics : DATATYPE_TACTICS =