diff -r 0579dec9f8ba -r 623d4831c8cf src/HOL/Tools/Groebner_Basis/normalizer_data.ML
--- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Wed Mar 25 21:35:49 2009 +0100
+++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Thu Mar 26 14:14:02 2009 +0100
@@ -191,16 +191,17 @@
 
 in
 
-val attribute =
-  Scan.lift (Args.$$$ delN >> K del) ||
-    ((keyword2 semiringN opsN |-- terms) --
-     (keyword2 semiringN rulesN |-- thms)) --
-    (optional (keyword2 ringN opsN |-- terms) --
-     optional (keyword2 ringN rulesN |-- thms)) --
-    optional (keyword2 idomN rulesN |-- thms) --
-    optional (keyword2 idealN rulesN |-- thms)
-    >> (fn (((sr, r), id), idl) => 
-          add {semiring = sr, ring = r, idom = id, ideal = idl});
+val normalizer_setup =
+  Attrib.setup @{binding normalizer}
+    (Scan.lift (Args.$$$ delN >> K del) ||
+      ((keyword2 semiringN opsN |-- terms) --
+       (keyword2 semiringN rulesN |-- thms)) --
+      (optional (keyword2 ringN opsN |-- terms) --
+       optional (keyword2 ringN rulesN |-- thms)) --
+      optional (keyword2 idomN rulesN |-- thms) --
+      optional (keyword2 idealN rulesN |-- thms)
+      >> (fn (((sr, r), id), idl) => add {semiring = sr, ring = r, idom = id, ideal = idl}))
+    "semiring normalizer data";
 
 end;
 
@@ -208,7 +209,7 @@
 (* theory setup *)
 
 val setup =
-  Attrib.setup @{binding normalizer} attribute "semiring normalizer data" #>
+  normalizer_setup #>
   Attrib.setup @{binding algebra} (Attrib.add_del add_ss del_ss) "pre-simplification for algebra";
 
 end;