src/ZF/Tools/typechk.ML

--- a/src/ZF/Tools/typechk.ML	Sun Jul 29 14:29:52 2007 +0200
+++ b/src/ZF/Tools/typechk.ML	Sun Jul 29 14:29:54 2007 +0200
@@ -49,7 +49,7 @@
   val extend = I;
 
   fun merge _ (TC {rules, net}, TC {rules = rules', net = net'}) =
-    TC {rules = Drule.merge_rules (rules, rules'),
+    TC {rules = Thm.merge_thms (rules, rules'),
         net = Net.merge Thm.eq_thm_prop (net, net')};
 );