src/HOL/Library/comm_ring.ML
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,