# HG changeset patch
# User wenzelm
# Date 968172652 -7200
# Node ID 96138f29545ec2ca50958bc4fc67933b3a49b56f
# Parent  b2a6d854d6dabc40dcc5b165b9b5f6ed540913d3
improved add_rules;

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;