src/ZF/Tools/typechk.ML

 datatype tcset =
     TC of {rules: thm list,     (*the type-checking rules*)
            net: thm Net.net};   (*discrimination net of the same rules*)
 
 
-val mem_thm = gen_mem eq_thm
-and rem_thm = gen_rem eq_thm;
+val mem_thm = gen_mem Drule.eq_thm_prop
+and rem_thm = gen_rem Drule.eq_thm_prop;
 
 fun addTC (cs as TC{rules, net}, th) =
   if mem_thm (th, rules) then
          (warning ("Ignoring duplicate type-checking rule\n" ^
                    string_of_thm th);

          net = Net.insert_term ((concl_of th, th), net, K false)};
 
 
 fun delTC (cs as TC{rules, net}, th) =
   if mem_thm (th, rules) then
-      TC{net = Net.delete_term ((concl_of th, th), net, eq_thm),
+      TC{net = Net.delete_term ((concl_of th, th), net, Drule.eq_thm_prop),
          rules  = rem_thm (rules,th)}
   else (warning ("No such type-checking rule\n" ^ (string_of_thm th));
         cs);
 
 val op addTCs = foldl addTC;

                           APPEND typecheck_step_tac tcset)));
 
 
 
 fun merge_tc (TC{rules,net}, TC{rules=rules',net=net'}) =
-    TC {rules = gen_union eq_thm (rules,rules'),
-        net = Net.merge (net, net', eq_thm)};
+    TC {rules = gen_union Drule.eq_thm_prop (rules,rules'),
+        net = Net.merge (net, net', Drule.eq_thm_prop)};
 
 (*print tcsets*)
 fun print_tc (TC{rules,...}) =
     Pretty.writeln
        (Pretty.big_list "type-checking rules:" (map Display.pretty_thm rules));