--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML Thu May 06 16:32:21 2010 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML Thu May 06 16:40:02 2010 +0200
@@ -113,11 +113,6 @@
fun del_data key = apsnd (remove eq_data (key, []));
val del = Thm.declaration_attribute (Data.map o del_data);
-val add_ss = Thm.declaration_attribute
- (fn th => Data.map (fn (ss,data) => (ss addsimps [th], data)));
-
-val del_ss = Thm.declaration_attribute
- (fn th => Data.map (fn (ss,data) => (ss delsimps [th], data)));
fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules),
field = (f_ops, f_rules), idom, ideal} =
@@ -872,8 +867,6 @@
(* theory setup *)
-val setup =
- normalizer_setup #>
- Attrib.setup @{binding algebra} (Attrib.add_del add_ss del_ss) "pre-simplification for algebra";
+val setup = normalizer_setup
end;