src/Provers/classical.ML
changeset 12109 bd6eb9194a5d
parent 12053 7e2e84e503ce
child 12311 ce5f9e61c037
--- a/src/Provers/classical.ML	Thu Nov 08 23:57:22 2001 +0100
+++ b/src/Provers/classical.ML	Thu Nov 08 23:59:37 2001 +0100
@@ -922,6 +922,7 @@
 
   val empty = ref empty_cs;
   fun copy (ref cs) = (ref cs): T;            (*create new reference!*)
+  val finish = I;
   val prep_ext = copy;
   fun merge (ref cs1, ref cs2) = ref (merge_cs (cs1, cs2));
   fun print _ (ref cs) = print_cs cs;