diff -r 978dcf30c3dd -r 90eff1b52428 src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Wed Jul 13 16:07:18 2005 +0200
+++ b/src/ZF/Tools/typechk.ML	Wed Jul 13 16:07:21 2005 +0200
@@ -58,12 +58,12 @@
           cs)
   else
       TC{rules  = th::rules,
-         net = Net.insert_term ((concl_of th, th), net, K false)};
+         net = Net.insert_term (K false) (concl_of th, th) net};
 
 
 fun delTC (cs as TC{rules, net}, th) =
   if mem_thm (th, rules) then
-      TC{net = Net.delete_term ((concl_of th, th), net, Drule.eq_thm_prop),
+      TC{net = Net.delete_term Drule.eq_thm_prop (concl_of th, th) net,
          rules  = rem_thm (rules,th)}
   else (warning ("No such type-checking rule\n" ^ (string_of_thm th));
         cs);
@@ -113,7 +113,7 @@
 
 fun merge_tc (TC{rules,net}, TC{rules=rules',net=net'}) =
     TC {rules = gen_union Drule.eq_thm_prop (rules,rules'),
-        net = Net.merge (net, net', Drule.eq_thm_prop)};
+        net = Net.merge Drule.eq_thm_prop (net, net')};
 
 (*print tcsets*)
 fun print_tc (TC{rules,...}) =