--- a/src/Provers/blast.ML Tue Feb 10 14:29:36 2015 +0100
+++ b/src/Provers/blast.ML Tue Feb 10 14:48:26 2015 +0100
@@ -488,8 +488,11 @@
(*Resolution/matching tactics: if upd then the proof state may be updated.
Matching makes the tactics more deterministic in the presence of Vars.*)
-fun emtac ctxt upd rl = TRACE ctxt rl (if upd then eresolve_tac [rl] else ematch_tac ctxt [rl]);
-fun rmtac ctxt upd rl = TRACE ctxt rl (if upd then resolve_tac [rl] else match_tac ctxt [rl]);
+fun emtac ctxt upd rl =
+ TRACE ctxt rl (if upd then eresolve_tac ctxt [rl] else ematch_tac ctxt [rl]);
+
+fun rmtac ctxt upd rl =
+ TRACE ctxt rl (if upd then resolve_tac ctxt [rl] else match_tac ctxt [rl]);
(*Tableau rule from elimination rule.
Flag "upd" says that the inference updated the branch.
@@ -624,7 +627,7 @@
(*Tactic. Convert *Goal* to negated assumption in FIRST position*)
fun negOfGoal_tac ctxt i =
- TRACE ctxt Data.ccontr (resolve_tac [Data.ccontr]) i THEN rotate_tac ~1 i;
+ TRACE ctxt Data.ccontr (resolve_tac ctxt [Data.ccontr]) i THEN rotate_tac ~1 i;
fun traceTerm ctxt t =
let val thy = Proof_Context.theory_of ctxt