src/Provers/Arith/fast_lin_arith.ML
changeset 12311 ce5f9e61c037
parent 12283 d42aa776889e
child 12932 3bda5306d262
--- a/src/Provers/Arith/fast_lin_arith.ML	Wed Nov 28 00:44:37 2001 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Nov 28 00:46:26 2001 +0100
@@ -100,7 +100,6 @@
   val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [],
                lessD = [], simpset = Simplifier.empty_ss};
   val copy = I;
-  val finish = I;
   val prep_ext = I;
 
   fun merge ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1,