diff -r ded0ff754037 -r 5283e349b339 src/HOL/Tools/semiring_normalizer.ML
--- a/src/HOL/Tools/semiring_normalizer.ML	Sun Feb 15 17:01:22 2015 +0100
+++ b/src/HOL/Tools/semiring_normalizer.ML	Sun Feb 15 17:01:22 2015 +0100
@@ -8,7 +8,6 @@
 sig
   type entry
   val match: Proof.context -> cterm -> entry option
-  val del: attribute
   val add: {semiring: cterm list * thm list, ring: cterm list * thm list,
     field: cterm list * thm list, idom: thm list, ideal: thm list} -> attribute
 
@@ -150,8 +149,6 @@
 val idealN = "ideal";
 val fieldN = "field";
 
-val del = Thm.declaration_attribute (Data.map o AList.delete Thm.eq_thm);
-
 fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), 
          field = (f_ops, f_rules), idom, ideal} =
   Thm.declaration_attribute (fn key => fn context => context |> Data.map
@@ -880,8 +877,7 @@
 val _ =
   Theory.setup
     (Attrib.setup @{binding normalizer}
-      (Scan.lift (Args.$$$ delN >> K del) ||
-        ((keyword2 semiringN opsN |-- terms) --
+      (((keyword2 semiringN opsN |-- terms) --
          (keyword2 semiringN rulesN |-- thms)) --
         (optional (keyword2 ringN opsN |-- terms) --
          optional (keyword2 ringN rulesN |-- thms)) --