changeset 28339 | 6f6fa16543f5 |
parent 28326 | ddd53738dae8 |
child 29273 | 285c00993bc2 |
--- 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);