Drule.merge_rules;

--- 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 _ _ = ();
 );
 

--- 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, ...}) =