src/Provers/blast.ML

 
 fun cond_tracing true msg = tracing (msg ())
   | cond_tracing false _ = ();
 
 fun TRACE ctxt rl tac i st =
-  (cond_tracing (Config.get ctxt trace) (fn () => Display.string_of_thm ctxt rl); tac i st);
+  (cond_tracing (Config.get ctxt trace) (fn () => Thm.string_of_thm ctxt rl); tac i st);
 
 (*Resolution/matching tactics: if upd then the proof state may be updated.
   Matching makes the tactics more deterministic in the presence of Vars.*)
 fun emtac ctxt upd rl =
   TRACE ctxt rl (if upd then eresolve_tac ctxt [rl] else ematch_tac ctxt [rl]);

       rot_subgoals_tac (rot, #2 trl) i
   in SOME (trl, tac) end
   handle
     ElimBadPrem => (*reject: prems don't preserve conclusion*)
       (if Context_Position.is_visible ctxt then
-        warning ("Ignoring weak elimination rule\n" ^ Display.string_of_thm ctxt rl0)
+        warning ("Ignoring weak elimination rule\n" ^ Thm.string_of_thm ctxt rl0)
        else ();
        Option.NONE)
   | ElimBadConcl => (*ignore: conclusion is not just a variable*)
       (cond_tracing (Config.get ctxt trace)
         (fn () => "Ignoring ill-formed elimination rule:\n" ^
-          "conclusion should be a variable\n" ^ Display.string_of_thm ctxt rl0);
+          "conclusion should be a variable\n" ^ Thm.string_of_thm ctxt rl0);
        Option.NONE);
 
 
 (*** Conversion of Introduction Rules ***)