src/Pure/drule.ML
changeset 9862 96138f29545e
parent 9829 bf49c3796599
child 10403 2955ee2424ce
     1.1 --- a/src/Pure/drule.ML	Tue Sep 05 18:50:30 2000 +0200
     1.2 +++ b/src/Pure/drule.ML	Tue Sep 05 18:50:52 2000 +0200
     1.3 @@ -433,8 +433,8 @@
     1.4  val size_of_thm = size_of_term o #prop o rep_thm;
     1.5  
     1.6  (*maintain lists of theorems --- preserving canonical order*)
     1.7 -val add_rules = Library.generic_extend Thm.eq_thm I I;
     1.8  fun del_rules rs rules = Library.gen_rems Thm.eq_thm (rules, rs);
     1.9 +fun add_rules rs rules = rs @ del_rules rs rules;
    1.10  fun merge_rules (rules1, rules2) = Library.generic_merge Thm.eq_thm I I rules1 rules2;
    1.11  
    1.12