--- a/src/HOL/Algebra/ringsimp.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/Algebra/ringsimp.ML Sun Mar 15 15:59:44 2009 +0100
@@ -62,11 +62,11 @@
Thm.declaration_attribute
(fn _ => Data.map (AList.delete struct_eq s));
-val attribute = Attrib.syntax
- (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||
- Scan.succeed true) -- Scan.lift Args.name --
- Scan.repeat Args.term
- >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts)));
+val attribute =
+ Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||
+ Scan.succeed true) -- Scan.lift Args.name --
+ Scan.repeat Args.term
+ >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts));
(** Setup **)
@@ -74,6 +74,6 @@
val setup =
Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o algebra_tac))
"normalisation of algebraic structure" #>
- Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")];
+ Attrib.setup @{binding algebra} attribute "theorems controlling algebra method";
end;