| changeset 30510 | 4120fc59dd85 |
| parent 30164 | 9321f7b70450 |
| child 30552 | 58db56278478 |
--- a/src/Tools/coherent.ML Fri Mar 13 19:53:09 2009 +0100 +++ b/src/Tools/coherent.ML Fri Mar 13 19:58:26 2009 +0100 @@ -225,7 +225,7 @@ 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");