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