diff -r a1b3784f8129 -r cc06f17d8057 src/HOL/Tools/semiring_normalizer.ML
--- a/src/HOL/Tools/semiring_normalizer.ML	Sun Aug 18 19:59:19 2013 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML	Sun Aug 18 20:41:47 2013 +0200
@@ -179,6 +179,9 @@
       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 =>
@@ -188,7 +191,7 @@
     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 =
@@ -258,14 +261,16 @@
                 @{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"};