src/Provers/Arith/fast_lin_arith.ML
changeset 13105 3d1e7a199bdc
parent 12932 3bda5306d262
child 13186 ef8ed6adcb38
--- a/src/Provers/Arith/fast_lin_arith.ML	Tue May 07 14:24:30 2002 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Tue May 07 14:26:32 2002 +0200
@@ -107,7 +107,8 @@
              {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 = gen_merge_lists' (eq_thm o pairself fst) mult_mono_thms1 mult_mono_thms2,
+     mult_mono_thms = gen_merge_lists' (Drule.eq_thm_prop 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)};