src/Provers/blast.ML

 fun TRACE ctxt rl tac i st =
   (cond_tracing (Config.get ctxt trace) (fn () => Display.string_of_thm ctxt rl); tac i st);
 
 (*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.
   Flag "dup" requests duplication of the affected formula.*)
 fun fromRule (state as State {ctxt, ...}) vars rl =

   There can be at most one--this function could be made more efficient.*)
 fun negOfGoals pairs = map (fn (Gs,haz) => (map negOfGoal2 Gs, haz)) pairs;
 
 (*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
       val t' = norm (negOfGoal t)
       val stm = string_of ctxt 8 t'