# HG changeset patch
# User wenzelm
# Date 1139004750 -3600
# Node ID b05a2952de73d7c28a7c2898bf17d482b818d3e8
# Parent  f47c46d7d654f6b7a140a2adcebf64427c3e2971
removed add/del_rules;

diff -r f47c46d7d654 -r b05a2952de73 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Feb 03 23:12:28 2006 +0100
+++ b/src/Pure/drule.ML	Fri Feb 03 23:12:30 2006 +0100
@@ -99,8 +99,6 @@
   val compose_single: thm * int * thm -> thm
   val add_rule: thm -> thm list -> thm list
   val del_rule: thm -> thm list -> thm list
-  val add_rules: thm list -> thm list -> thm list
-  val del_rules: thm list -> thm list -> thm list
   val merge_rules: thm list * thm list -> thm list
   val imp_cong_rule: thm -> thm -> thm
   val beta_eta_conversion: cterm -> thm
@@ -588,11 +586,9 @@
 val size_of_thm = size_of_term o Thm.full_prop_of;
 
 (*maintain lists of theorems --- preserving canonical order*)
-fun del_rules rs rules = Library.gen_rems eq_thm_prop (rules, rs);
-fun add_rules rs rules = rs @ del_rules rs rules;
-val del_rule = del_rules o single;
-val add_rule = add_rules o single;
-fun merge_rules (rules1, rules2) = gen_merge_lists' eq_thm_prop rules1 rules2;
+val del_rule = remove eq_thm_prop;
+fun add_rule th = cons th o del_rule th;
+val merge_rules = Library.merge eq_thm_prop;
 
 (*weak_eq_thm: ignores variable renaming and (some) type variable renaming*)
 val weak_eq_thm = Thm.eq_thm o pairself (forall_intr_vars o freezeT);