1.1 --- a/src/Provers/coherent.ML	Tue Sep 23 18:11:45 2008 +0200
     1.2 +++ b/src/Provers/coherent.ML	Tue Sep 23 18:31:33 2008 +0200
     1.3 @@ -223,7 +223,7 @@
     1.4           NONE => no_tac
     1.5         | SOME prf =>
     1.6             rtac (thm_of_cl_prf (ProofContext.theory_of context) concl [] prf) 1
     1.7 -    end) ctxt 1) ctxt;
     1.8 +    end) context 1) ctxt;
     1.9  
    1.10  fun coherent_meth rules ctxt =
    1.11    Method.METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1);