# HG changeset patch
# User wenzelm
# Date 1006617300 -3600
# Node ID d42aa776889ef4f93062e9f0fc600fb692eb73e1
# Parent  f98beaaa7c4ff685f724100a6000ce9cd7799a54
gen_merge_lists';

diff -r f98beaaa7c4f -r d42aa776889e src/Provers/Arith/fast_lin_arith.ML
--- 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)};
diff -r f98beaaa7c4f -r d42aa776889e src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sat Nov 24 16:54:32 2001 +0100
+++ b/src/Pure/drule.ML	Sat Nov 24 16:55:00 2001 +0100
@@ -489,7 +489,7 @@
 (*maintain lists of theorems --- preserving canonical order*)
 fun del_rules rs rules = Library.gen_rems Thm.eq_thm (rules, rs);
 fun add_rules rs rules = rs @ del_rules rs rules;
-fun merge_rules (rules1, rules2) = Library.generic_merge Thm.eq_thm I I rules1 rules2;
+fun merge_rules (rules1, rules2) = gen_merge_lists' Thm.eq_thm rules1 rules2;
 
 
 (** Mark Staples's weaker version of eq_thm: ignores variable renaming and