gen_merge_lists';
authorwenzelm
Sat Nov 24 16:55:00 2001 +0100 (2001-11-24)
changeset 12283d42aa776889e
parent 12282 f98beaaa7c4f
child 12284 131e743d168a
gen_merge_lists';
src/Provers/Arith/fast_lin_arith.ML
src/Pure/drule.ML
     1.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Sat Nov 24 16:54:32 2001 +0100
     1.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Sat Nov 24 16:55:00 2001 +0100
     1.3 @@ -108,7 +108,7 @@
     1.4               {add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2,
     1.5                lessD = lessD2, simpset = simpset2}) =
     1.6      {add_mono_thms = Drule.merge_rules (add_mono_thms1, add_mono_thms2),
     1.7 -     mult_mono_thms= generic_merge (eq_thm o pairself fst) I I mult_mono_thms1 mult_mono_thms2,
     1.8 +     mult_mono_thms = gen_merge_lists' (eq_thm o pairself fst) mult_mono_thms1 mult_mono_thms2,
     1.9       inj_thms = Drule.merge_rules (inj_thms1, inj_thms2),
    1.10       lessD = Drule.merge_rules (lessD1, lessD2),
    1.11       simpset = Simplifier.merge_ss (simpset1, simpset2)};
     2.1 --- a/src/Pure/drule.ML	Sat Nov 24 16:54:32 2001 +0100
     2.2 +++ b/src/Pure/drule.ML	Sat Nov 24 16:55:00 2001 +0100
     2.3 @@ -489,7 +489,7 @@
     2.4  (*maintain lists of theorems --- preserving canonical order*)
     2.5  fun del_rules rs rules = Library.gen_rems Thm.eq_thm (rules, rs);
     2.6  fun add_rules rs rules = rs @ del_rules rs rules;
     2.7 -fun merge_rules (rules1, rules2) = Library.generic_merge Thm.eq_thm I I rules1 rules2;
     2.8 +fun merge_rules (rules1, rules2) = gen_merge_lists' Thm.eq_thm rules1 rules2;
     2.9  
    2.10  
    2.11  (** Mark Staples's weaker version of eq_thm: ignores variable renaming and