--- 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;