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