src/Tools/coherent.ML

        | SOME prf =>
            rtac (thm_of_cl_prf (ProofContext.theory_of context) concl [] prf) 1
     end) context 1) ctxt;
 
 fun coherent_meth rules ctxt =
-  Method.METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1);
+  METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1);
 
 val setup = Method.add_method
   ("coherent", Method.thms_ctxt_args coherent_meth, "prove coherent formula");
 
 end;