diff -r 39acf19e9f3a -r 30e2ffbba718 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Provers/blast.ML	Tue Jul 21 01:03:18 2009 +0200
@@ -492,7 +492,9 @@
 end;
 
 
-fun TRACE rl tac st i = if !trace then (Display.prth rl; tac st i) else tac st i;
+fun TRACE rl tac st i =
+  if !trace then (writeln (Display.string_of_thm_without_context rl); tac st i)
+  else tac st i;
 
 (*Resolution/matching tactics: if upd then the proof state may be updated.
   Matching makes the tactics more deterministic in the presence of Vars.*)
@@ -509,14 +511,16 @@
         THEN
         rot_subgoals_tac (rot, #2 trl) i
   in Option.SOME (trl, tac) end
-  handle ElimBadPrem => (*reject: prems don't preserve conclusion*)
-            (warning("Ignoring weak elimination rule\n" ^ Display.string_of_thm rl);
-             Option.NONE)
-       | ElimBadConcl => (*ignore: conclusion is not just a variable*)
-           (if !trace then (warning("Ignoring ill-formed elimination rule:\n" ^
-                       "conclusion should be a variable\n" ^ Display.string_of_thm rl))
-            else ();
-            Option.NONE);
+  handle
+    ElimBadPrem => (*reject: prems don't preserve conclusion*)
+      (warning ("Ignoring weak elimination rule\n" ^ Display.string_of_thm_global thy rl);
+        Option.NONE)
+  | ElimBadConcl => (*ignore: conclusion is not just a variable*)
+      (if !trace then
+        (warning ("Ignoring ill-formed elimination rule:\n" ^
+          "conclusion should be a variable\n" ^ Display.string_of_thm_global thy rl))
+       else ();
+       Option.NONE);
 
 
 (*** Conversion of Introduction Rules ***)