--- a/src/HOL/Tools/semiring_normalizer.ML Fri Oct 22 23:45:20 2010 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML Sun Oct 24 20:19:00 2010 +0200
@@ -826,7 +826,7 @@
end;
val nat_exp_ss =
- HOL_basic_ss addsimps (@{thms nat_number} @ @{thms nat_arith} @ @{thms arith_simps} @ @{thms rel_simps})
+ HOL_basic_ss addsimps (@{thms eval_nat_numeral} @ @{thms nat_arith} @ @{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;