src/Provers/simplifier.ML
changeset 12109 bd6eb9194a5d
parent 11938 7b594aba1300
child 12282 f98beaaa7c4f
--- a/src/Provers/simplifier.ML	Thu Nov 08 23:57:22 2001 +0100
+++ b/src/Provers/simplifier.ML	Thu Nov 08 23:59:37 2001 +0100
@@ -313,6 +313,7 @@
 
   val empty = ref empty_ss;
   fun copy (ref ss) = (ref ss): T;            (*create new reference!*)
+  val finish = I;
   val prep_ext = copy;
   fun merge (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
   fun print _ (ref ss) = print_ss ss;