src/HOL/Tools/semiring_normalizer.ML

       raise THM ("No data entry for structure key", 0, [key]);
     val fns = {is_const = is_const phi, dest_const = dest_const phi,
       mk_const = mk_const phi, conv = conv phi};
   in AList.map_entry Thm.eq_thm key (apsnd (K fns)) data end);
 
+val semiring_norm_ss =
+  simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms semiring_norm});
+
 fun semiring_funs key = funs key
    {is_const = fn phi => can HOLogic.dest_number o Thm.term_of,
     dest_const = fn phi => fn ct =>
       Rat.rat_of_int (snd
         (HOLogic.dest_number (Thm.term_of ct)
           handle TERM _ => error "ring_dest_const")),
     mk_const = fn phi => fn cT => fn x => Numeral.mk_cnumber cT
       (case Rat.quotient_of_rat x of (i, 1) => i | _ => error "int_of_rat: bad int"),
     conv = fn phi => fn ctxt =>
-      Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms semiring_norm})
+      Simplifier.rewrite (put_simpset semiring_norm_ss ctxt)
       then_conv Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms numeral_1_eq_1})};
 
 fun field_funs key =
   let
     fun numeral_is_const ct =

   zero1_numeral_conv ctxt then_conv cv then_conv numeral01_conv ctxt;
 val natarith = [@{thm "numeral_plus_numeral"}, @{thm "diff_nat_numeral"},
                 @{thm "numeral_times_numeral"}, @{thm "numeral_eq_iff"}, 
                 @{thm "numeral_less_iff"}];
 
+val nat_add_ss =
+  simpset_of 
+    (put_simpset HOL_basic_ss @{context}
+       addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps}
+             @ [@{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc},
+                 @{thm add_numeral_left}, @{thm Suc_eq_plus1}]
+             @ map (fn th => th RS sym) @{thms numerals});
+
 fun nat_add_conv ctxt =
-  zerone_conv ctxt
-    (Simplifier.rewrite 
-      (put_simpset HOL_basic_ss ctxt
-         addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps}
-               @ [@{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc},
-                   @{thm add_numeral_left}, @{thm Suc_eq_plus1}]
-               @ map (fn th => th RS sym) @{thms numerals}));
+  zerone_conv ctxt (Simplifier.rewrite (put_simpset nat_add_ss ctxt));
 
 val zeron_tm = @{cterm "0::nat"};
 val onen_tm  = @{cterm "1::nat"};
 val true_tm = @{cterm "True"};