# HG changeset patch
# User wenzelm
# Date 1153855078 -7200
# Node ID 46f5ef758422f1cbff06fc544fa185fe783f2b97
# Parent  956cd30ef3bebbe59df6b74672f7599e7fd518ff
Drule.merge_rules;

diff -r 956cd30ef3be -r 46f5ef758422 src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Tue Jul 25 16:51:26 2006 +0200
+++ b/src/CCL/Wfd.thy	Tue Jul 25 21:17:58 2006 +0200
@@ -504,7 +504,7 @@
   type T = thm list;
   val empty = [];
   val extend = I;
-  fun merge _ (rules1, rules2) = gen_union Drule.eq_thm_prop (rules1, rules2);
+  fun merge _ = Drule.merge_rules;
   fun print _ _ = ();
 );
 
diff -r 956cd30ef3be -r 46f5ef758422 src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Tue Jul 25 16:51:26 2006 +0200
+++ b/src/ZF/Tools/typechk.ML	Tue Jul 25 21:17:58 2006 +0200
@@ -50,7 +50,7 @@
   val extend = I;
 
   fun merge _ (TC {rules, net}, TC {rules = rules', net = net'}) =
-    TC {rules = gen_union Drule.eq_thm_prop (rules, rules'),
+    TC {rules = Drule.merge_rules (rules, rules'),
         net = Net.merge Drule.eq_thm_prop (net, net')};
 
   fun print context (TC {rules, ...}) =