--- a/ProgTutorial/Tactical.thy	Tue Mar 20 09:39:44 2012 +0000
+++ b/ProgTutorial/Tactical.thy	Mon Apr 30 12:33:17 2012 +0100
@@ -1992,8 +1992,7 @@
 let
   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 eval_nat_numeral} @ @{thms neg_simps} @ @{thms plus_nat.simps}
+  val num_ss = HOL_ss addsimps @{thms semiring_norm}
 in
   Goal.prove ctxt [] [] goal (K (simp_tac num_ss 1))
 end*}
@@ -2017,7 +2016,7 @@
 let 
   val ctxt = Simplifier.the_context ss
 in
-  SOME (get_thm ctxt (t, dest_suc_trm t))
+  SOME (get_thm_alt ctxt (t, dest_suc_trm t))
   handle TERM _ => NONE
 end*}