--- a/src/Provers/Arith/fast_lin_arith.ML Sat Nov 24 16:54:32 2001 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML Sat Nov 24 16:55:00 2001 +0100
@@ -108,7 +108,7 @@
{add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2,
lessD = lessD2, simpset = simpset2}) =
{add_mono_thms = Drule.merge_rules (add_mono_thms1, add_mono_thms2),
- mult_mono_thms= generic_merge (eq_thm o pairself fst) I I mult_mono_thms1 mult_mono_thms2,
+ mult_mono_thms = gen_merge_lists' (eq_thm o pairself fst) mult_mono_thms1 mult_mono_thms2,
inj_thms = Drule.merge_rules (inj_thms1, inj_thms2),
lessD = Drule.merge_rules (lessD1, lessD2),
simpset = Simplifier.merge_ss (simpset1, simpset2)};