changeset 30510 | 4120fc59dd85 |
parent 29265 | 5b4247055bd7 |
child 31021 | 53642251a04f |
--- a/src/HOL/Library/comm_ring.ML Fri Mar 13 19:53:09 2009 +0100 +++ b/src/HOL/Library/comm_ring.ML Fri Mar 13 19:58:26 2009 +0100 @@ -101,7 +101,7 @@ end); val comm_ring_meth = - Method.ctxt_args (Method.SIMPLE_METHOD' o comm_ring_tac); + Method.ctxt_args (SIMPLE_METHOD' o comm_ring_tac); val setup = Method.add_method ("comm_ring", comm_ring_meth,