# 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;