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