src/Provers/simplifier.ML
changeset 12311 ce5f9e61c037
parent 12282 f98beaaa7c4f
child 13462 56610e2ba220
--- a/src/Provers/simplifier.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/Provers/simplifier.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -312,7 +312,6 @@
 
   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;