--- 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);