# HG changeset patch
# User berghofe
# Date 1222187493 -7200
# Node ID 6f6fa16543f54bbf9e0a2f4906365982d92ce821
# Parent  e58ec46d50bcebc3c32c8e0218b8ecc4e0f03d44
Corrected call of SUBPROOF in coherent_tac that used wrong context.

diff -r e58ec46d50bc -r 6f6fa16543f5 src/Provers/coherent.ML
--- a/src/Provers/coherent.ML	Tue Sep 23 18:11:45 2008 +0200
+++ b/src/Provers/coherent.ML	Tue Sep 23 18:31:33 2008 +0200
@@ -223,7 +223,7 @@
          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);