diff -r 0c5cd369a643 -r 50b60f501b05 src/Provers/blast.ML
--- 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