diff -r b2a6d854d6da -r 96138f29545e src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Sep 05 18:50:30 2000 +0200
+++ b/src/Pure/drule.ML	Tue Sep 05 18:50:52 2000 +0200
@@ -433,8 +433,8 @@
 val size_of_thm = size_of_term o #prop o rep_thm;
 
 (*maintain lists of theorems --- preserving canonical order*)
-val add_rules = Library.generic_extend Thm.eq_thm I I;
 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;