src/ZF/Tools/typechk.ML
changeset 16800 90eff1b52428
parent 16458 4c6fd0c01d28
child 17057 0934ac31985f
     1.1 --- a/src/ZF/Tools/typechk.ML	Wed Jul 13 16:07:18 2005 +0200
     1.2 +++ b/src/ZF/Tools/typechk.ML	Wed Jul 13 16:07:21 2005 +0200
     1.3 @@ -58,12 +58,12 @@
     1.4            cs)
     1.5    else
     1.6        TC{rules  = th::rules,
     1.7 -         net = Net.insert_term ((concl_of th, th), net, K false)};
     1.8 +         net = Net.insert_term (K false) (concl_of th, th) net};
     1.9  
    1.10  
    1.11  fun delTC (cs as TC{rules, net}, th) =
    1.12    if mem_thm (th, rules) then
    1.13 -      TC{net = Net.delete_term ((concl_of th, th), net, Drule.eq_thm_prop),
    1.14 +      TC{net = Net.delete_term Drule.eq_thm_prop (concl_of th, th) net,
    1.15           rules  = rem_thm (rules,th)}
    1.16    else (warning ("No such type-checking rule\n" ^ (string_of_thm th));
    1.17          cs);
    1.18 @@ -113,7 +113,7 @@
    1.19  
    1.20  fun merge_tc (TC{rules,net}, TC{rules=rules',net=net'}) =
    1.21      TC {rules = gen_union Drule.eq_thm_prop (rules,rules'),
    1.22 -        net = Net.merge (net, net', Drule.eq_thm_prop)};
    1.23 +        net = Net.merge Drule.eq_thm_prop (net, net')};
    1.24  
    1.25  (*print tcsets*)
    1.26  fun print_tc (TC{rules,...}) =