diff -r c7af3d651658 -r ce00f2fef556 src/HOL/Tools/semiring_normalizer.ML
--- a/src/HOL/Tools/semiring_normalizer.ML	Mon Nov 04 18:08:47 2013 +0100
+++ b/src/HOL/Tools/semiring_normalizer.ML	Mon Nov 04 20:10:06 2013 +0100
@@ -848,7 +848,7 @@
 val nat_exp_ss =
   simpset_of
    (put_simpset HOL_basic_ss @{context}
-    addsimps (@{thms eval_nat_numeral} @ @{thms nat_arith} @ @{thms arith_simps} @ @{thms rel_simps})
+    addsimps (@{thms eval_nat_numeral} @ @{thms diff_nat_numeral} @ @{thms arith_simps} @ @{thms rel_simps})
     addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}]);
 
 fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS;