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,