src/Provers/blast.ML
changeset 26928 ca87aff1ad2d
parent 25365 4e7a1dabd7ef
child 26938 64e850c3da9e
--- a/src/Provers/blast.ML	Fri May 16 23:25:37 2008 +0200
+++ b/src/Provers/blast.ML	Sat May 17 13:54:30 2008 +0200
@@ -495,7 +495,7 @@
 end;
 
 
-fun TRACE rl tac st i = if !trace then (prth rl; tac st i) else tac st i;
+fun TRACE rl tac st i = if !trace then (Display.prth 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.*)
@@ -513,11 +513,11 @@
         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" ^ string_of_thm rl);
+            (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" ^ string_of_thm rl))
+                       "conclusion should be a variable\n" ^ Display.string_of_thm rl))
             else ();
             Option.NONE);