--- a/ProgTutorial/Recipes/Timing.thy	Fri Oct 29 13:10:33 2010 +0200
+++ b/ProgTutorial/Recipes/Timing.thy	Fri Oct 29 13:16:45 2010 +0200
@@ -52,7 +52,7 @@
 
 lemma "ackermann (3, 4) = 125"
 apply(tactic {* 
-  timing_wrapper (simp_tac (@{simpset} addsimps @{thms "nat_number"}) 1) *})
+  timing_wrapper (simp_tac (@{simpset} addsimps @{thms "eval_nat_numeral"}) 1) *})
 done
 
 text {*
@@ -69,4 +69,4 @@
 
 
 
-end
\ No newline at end of file
+end

--- a/ProgTutorial/Tactical.thy	Fri Oct 29 13:10:33 2010 +0200
+++ b/ProgTutorial/Tactical.thy	Fri Oct 29 13:16:45 2010 +0200
@@ -1989,7 +1989,7 @@
   val num = HOLogic.mk_number @{typ "nat"} n
   val goal = Logic.mk_equals (t, num)
   val num_ss = HOL_ss addsimps [@{thm One_nat_def}, @{thm Let_def}] @ 
-          @{thms nat_number} @ @{thms neg_simps} @ @{thms plus_nat.simps}
+          @{thms eval_nat_numeral} @ @{thms neg_simps} @ @{thms plus_nat.simps}
 in
   Goal.prove ctxt [] [] goal (K (simp_tac num_ss 1))
 end*}