src/ZF/Tools/typechk.ML

  {rules: thm list,     (*the type-checking rules*)
   net: thm Net.net};   (*discrimination net of the same rules*)
 
 fun add_rule ctxt th (tcs as TC {rules, net}) =
   if member Thm.eq_thm_prop rules th then
-    (warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm ctxt th); tcs)
+    (warning ("Ignoring duplicate type-checking rule\n" ^ Thm.string_of_thm ctxt th); tcs)
   else
     TC {rules = th :: rules, net = Net.insert_term (K false) (Thm.concl_of th, th) net};
 
 fun del_rule ctxt th (tcs as TC {rules, net}) =
   if member Thm.eq_thm_prop rules th then
     TC {net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net,
       rules = remove Thm.eq_thm_prop th rules}
-  else (warning ("No such type-checking rule\n" ^ Display.string_of_thm ctxt th); tcs);
+  else (warning ("No such type-checking rule\n" ^ Thm.string_of_thm ctxt th); tcs);
 
 
 (* generic data *)
 
 structure Data = Generic_Data

 val tcset_of = Data.get o Context.Proof;
 
 fun print_tcset ctxt =
   let val TC {rules, ...} = tcset_of ctxt in
     Pretty.writeln (Pretty.big_list "type-checking rules:"
-      (map (Display.pretty_thm_item ctxt) rules))
+      (map (Thm.pretty_thm_item ctxt) rules))
   end;
 
 
 (* tactics *)