src/ZF/Tools/induct_tacs.ML
changeset 6556 daa00919502b
parent 6141 a6922171b396
child 6851 526c0b90bcef
--- a/src/ZF/Tools/induct_tacs.ML	Fri Apr 30 18:09:33 1999 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Fri Apr 30 18:10:03 1999 +0200
@@ -37,6 +37,7 @@
   type T = datatype_info Symtab.table;
 
   val empty = Symtab.empty;
+  val copy = I;
   val prep_ext = I;
   val merge: T * T -> T = Symtab.merge (K true);
 
@@ -63,6 +64,7 @@
   type T = constructor_info Symtab.table
 
   val empty = Symtab.empty
+  val copy = I;
   val prep_ext = I
   val merge: T * T -> T = Symtab.merge (K true)