diff -r 0b6217fda81b -r abe08fb15a12 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Provers/blast.ML	Fri Sep 25 20:37:59 2015 +0200
@@ -484,7 +484,7 @@
   | 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.*)
@@ -509,13 +509,13 @@
   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);