src/Provers/coherent.ML

       case valid context (map mk_rule (prems' @ prems @ rules)) (term_of concl)
            (mk_dom xs) Net.empty 0 0 of
          NONE => no_tac
        | SOME prf =>
            rtac (thm_of_cl_prf (ProofContext.theory_of context) concl [] prf) 1
-    end) ctxt 1) ctxt;
+    end) context 1) ctxt;
 
 fun coherent_meth rules ctxt =
   Method.METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1);
 
 val setup = Method.add_method