src/Tools/coherent.ML
changeset 30510 4120fc59dd85
parent 30164 9321f7b70450
child 30552 58db56278478
     1.1 --- a/src/Tools/coherent.ML	Fri Mar 13 19:53:09 2009 +0100
     1.2 +++ b/src/Tools/coherent.ML	Fri Mar 13 19:58:26 2009 +0100
     1.3 @@ -225,7 +225,7 @@
     1.4      end) context 1) ctxt;
     1.5  
     1.6  fun coherent_meth rules ctxt =
     1.7 -  Method.METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1);
     1.8 +  METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1);
     1.9  
    1.10  val setup = Method.add_method
    1.11    ("coherent", Method.thms_ctxt_args coherent_meth, "prove coherent formula");