--- 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*}