src/HOL/Tools/inductive_package.ML
changeset 6556 daa00919502b
parent 6521 16c425fc00cb
child 6723 f342449d73ca
--- a/src/HOL/Tools/inductive_package.ML	Fri Apr 30 18:09:33 1999 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Fri Apr 30 18:10:03 1999 +0200
@@ -161,6 +161,7 @@
   type T = inductive_info Symtab.table;
 
   val empty = Symtab.empty;
+  val copy = I;
   val prep_ext = I;
   val merge: T * T -> T = Symtab.merge (K true);