--- a/src/HOL/Tools/primrec_package.ML Thu Nov 08 23:57:22 2001 +0100
+++ b/src/HOL/Tools/primrec_package.ML Thu Nov 08 23:59:37 2001 +0100
@@ -47,6 +47,7 @@
val empty = Symtab.empty;
val copy = I;
+ val finish = I;
val prep_ext = I;
val merge: T * T -> T = Symtab.merge (K true);