# HG changeset patch
# User wenzelm
# Date 1414576721 -3600
# Node ID 19382bbfa93aeeaa189a61d4843fdb9158e570b4
# Parent  922a233805d26f97c2b38518601e24c714ea2ef0
modernized setup;
more standard module name;

diff -r 922a233805d2 -r 19382bbfa93a src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Wed Oct 29 10:35:00 2014 +0100
+++ b/src/HOL/Algebra/Ring.thy	Wed Oct 29 10:58:41 2014 +0100
@@ -391,10 +391,14 @@
 
 ML_file "ringsimp.ML"
 
-setup Algebra.attrib_setup
+attribute_setup algebra = {*
+  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 Ringsimp.add_struct (n, ts) else Ringsimp.del_struct (n, ts))
+*} "theorems controlling algebra method"
 
 method_setup algebra = {*
-  Scan.succeed (SIMPLE_METHOD' o Algebra.algebra_tac)
+  Scan.succeed (SIMPLE_METHOD' o Ringsimp.algebra_tac)
 *} "normalisation of algebraic structure"
 
 lemmas (in ring) ring_simprules
diff -r 922a233805d2 -r 19382bbfa93a src/HOL/Algebra/ringsimp.ML
--- a/src/HOL/Algebra/ringsimp.ML	Wed Oct 29 10:35:00 2014 +0100
+++ b/src/HOL/Algebra/ringsimp.ML	Wed Oct 29 10:58:41 2014 +0100
@@ -3,17 +3,17 @@
 Normalisation method for locales ring and cring.
 *)
 
-signature ALGEBRA =
+signature RINGSIMP =
 sig
   val print_structures: Proof.context -> unit
-  val attrib_setup: theory -> theory
+  val add_struct: string * term list -> attribute
+  val del_struct: string * term list -> attribute
   val algebra_tac: Proof.context -> int -> tactic
 end;
 
-structure Algebra: ALGEBRA =
+structure Ringsimp: RINGSIMP =
 struct
 
-
 (** Theory and context data **)
 
 fun struct_eq ((s1: string, ts1), (s2, ts2)) =
@@ -56,7 +56,7 @@
 
 (** Attribute **)
 
-fun add_struct_thm s =
+fun add_struct s =
   Thm.declaration_attribute
     (fn thm => Data.map (AList.map_default struct_eq (s, []) (insert Thm.eq_thm_prop thm)));
 
@@ -64,11 +64,4 @@
   Thm.declaration_attribute
     (fn _ => Data.map (AList.delete struct_eq s));
 
-val attrib_setup =
-  Attrib.setup @{binding algebra}
-    (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)))
-    "theorems controlling algebra method";
-
 end;