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