diff -r 0c5cd369a643 -r 50b60f501b05 src/Tools/coherent.ML
--- a/src/Tools/coherent.ML	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/Tools/coherent.ML	Tue Feb 10 14:48:26 2015 +0100
@@ -215,7 +215,7 @@
 (** external interface **)
 
 fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context = ctxt', ...} =>
-  resolve_tac [rulify_elim_conv ctxt' concl RS Drule.equal_elim_rule2] 1 THEN
+  resolve_tac ctxt' [rulify_elim_conv ctxt' concl RS Drule.equal_elim_rule2] 1 THEN
   SUBPROOF (fn {prems = prems', concl, context = ctxt'', ...} =>
     let
       val xs =
@@ -227,7 +227,7 @@
         valid ctxt'' (map (mk_rule ctxt'') (prems' @ prems @ rules)) (term_of concl)
           (mk_dom xs) Net.empty 0 0 of
         NONE => no_tac
-      | SOME prf => resolve_tac [thm_of_cl_prf ctxt'' concl [] prf] 1)
+      | SOME prf => resolve_tac ctxt'' [thm_of_cl_prf ctxt'' concl [] prf] 1)
     end) ctxt' 1) ctxt;
 
 val _ = Theory.setup