src/ZF/Tools/typechk.ML
changeset 13105 3d1e7a199bdc
parent 12311 ce5f9e61c037
child 15090 970c2668c694
     1.1 --- a/src/ZF/Tools/typechk.ML	Tue May 07 14:24:30 2002 +0200
     1.2 +++ b/src/ZF/Tools/typechk.ML	Tue May 07 14:26:32 2002 +0200
     1.3 @@ -46,8 +46,8 @@
     1.4             net: thm Net.net};   (*discrimination net of the same rules*)
     1.5  
     1.6  
     1.7 -val mem_thm = gen_mem eq_thm
     1.8 -and rem_thm = gen_rem eq_thm;
     1.9 +val mem_thm = gen_mem Drule.eq_thm_prop
    1.10 +and rem_thm = gen_rem Drule.eq_thm_prop;
    1.11  
    1.12  fun addTC (cs as TC{rules, net}, th) =
    1.13    if mem_thm (th, rules) then
    1.14 @@ -61,7 +61,7 @@
    1.15  
    1.16  fun delTC (cs as TC{rules, net}, th) =
    1.17    if mem_thm (th, rules) then
    1.18 -      TC{net = Net.delete_term ((concl_of th, th), net, eq_thm),
    1.19 +      TC{net = Net.delete_term ((concl_of th, th), net, Drule.eq_thm_prop),
    1.20           rules  = rem_thm (rules,th)}
    1.21    else (warning ("No such type-checking rule\n" ^ (string_of_thm th));
    1.22          cs);
    1.23 @@ -110,8 +110,8 @@
    1.24  
    1.25  
    1.26  fun merge_tc (TC{rules,net}, TC{rules=rules',net=net'}) =
    1.27 -    TC {rules = gen_union eq_thm (rules,rules'),
    1.28 -        net = Net.merge (net, net', eq_thm)};
    1.29 +    TC {rules = gen_union Drule.eq_thm_prop (rules,rules'),
    1.30 +        net = Net.merge (net, net', Drule.eq_thm_prop)};
    1.31  
    1.32  (*print tcsets*)
    1.33  fun print_tc (TC{rules,...}) =