diff -r 9455ecc7796d -r bca05b17b618 src/HOL/Algebra/ringsimp.ML
--- a/src/HOL/Algebra/ringsimp.ML	Fri Mar 13 23:32:40 2009 +0100
+++ b/src/HOL/Algebra/ringsimp.ML	Fri Mar 13 23:50:05 2009 +0100
@@ -72,8 +72,8 @@
 (** Setup **)
 
 val setup =
-  Method.add_methods [("algebra", Method.ctxt_args (SIMPLE_METHOD' o algebra_tac),
-    "normalisation of algebraic structure")] #>
+  Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o algebra_tac))
+    "normalisation of algebraic structure" #>
   Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")];
 
 end;