src/HOL/Tools/datatype_package.ML
changeset 6556 daa00919502b
parent 6479 b0448cab1b1e
child 6723 f342449d73ca
--- a/src/HOL/Tools/datatype_package.ML	Fri Apr 30 18:09:33 1999 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Fri Apr 30 18:10:03 1999 +0200
@@ -86,6 +86,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);