--- a/src/Provers/Arith/fast_lin_arith.ML Sun Jul 29 14:29:52 2007 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Sun Jul 29 14:29:54 2007 +0200
@@ -122,11 +122,11 @@
lessD = lessD1, neqE=neqE1, simpset = simpset1},
{add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2,
lessD = lessD2, neqE=neqE2, simpset = simpset2}) =
- {add_mono_thms = Drule.merge_rules (add_mono_thms1, add_mono_thms2),
- mult_mono_thms = Drule.merge_rules (mult_mono_thms1, mult_mono_thms2),
- inj_thms = Drule.merge_rules (inj_thms1, inj_thms2),
- lessD = Drule.merge_rules (lessD1, lessD2),
- neqE = Drule.merge_rules (neqE1, neqE2),
+ {add_mono_thms = Thm.merge_thms (add_mono_thms1, add_mono_thms2),
+ mult_mono_thms = Thm.merge_thms (mult_mono_thms1, mult_mono_thms2),
+ inj_thms = Thm.merge_thms (inj_thms1, inj_thms2),
+ lessD = Thm.merge_thms (lessD1, lessD2),
+ neqE = Thm.merge_thms (neqE1, neqE2),
simpset = Simplifier.merge_ss (simpset1, simpset2)};
);