diff -r cd28458c2add -r 501491d56798 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Fri Mar 01 00:49:15 2013 +0000
+++ b/ProgTutorial/Tactical.thy	Fri Apr 19 11:09:18 2013 +0100
@@ -407,7 +407,7 @@
 
 lemma 
   shows "False" and "Goldbach_conjecture"  
-apply(tactic {* Skip_Proof.cheat_tac @{theory} *})
+apply(tactic {* Skip_Proof.cheat_tac 1 *})
 txt{*\begin{minipage}{\textwidth}
      @{subgoals [display]}
      \end{minipage}*}
@@ -1344,7 +1344,7 @@
 
 lemma 
   shows "Suc (1 + 2) < 3 + 2"
-apply(tactic {* asm_full_simp_tac @{simpset} 1 *})
+apply(tactic {* asm_full_simp_tac @{context} 1 *})
 done
 
 text {*
@@ -1430,13 +1430,15 @@
 let
   val {simps, congs, procs, ...} = Raw_Simplifier.dest_ss ss
 
-  fun name_thm (nm, thm) =
+  fun name_sthm (nm, thm) =
+    Pretty.enclose (nm ^ ": ") "" [pretty_thm_no_vars ctxt thm]
+  fun name_cthm ((_, nm), thm) =
     Pretty.enclose (nm ^ ": ") "" [pretty_thm_no_vars ctxt thm]
   fun name_ctrm (nm, ctrm) =
     Pretty.enclose (nm ^ ": ") "" [pretty_cterms ctxt ctrm]
 
-  val pps = [Pretty.big_list "Simplification rules:" (map name_thm simps),
-             Pretty.big_list "Congruences rules:" (map name_thm congs),
+  val pps = [Pretty.big_list "Simplification rules:" (map name_sthm simps),
+             Pretty.big_list "Congruences rules:" (map name_cthm congs),
              Pretty.big_list "Simproc patterns:" (map name_ctrm procs)]
 in
   pps |> Pretty.chunks
@@ -1467,13 +1469,13 @@
   the simplification rule @{thm [source] Diff_Int} as follows:
 *}
 
-ML %grayML{*val ss1 = empty_ss addsimps [@{thm Diff_Int} RS @{thm eq_reflection}] *}
+ML %grayML{*val ss1 = put_simpset empty_ss @{context} addsimps [@{thm Diff_Int} RS @{thm eq_reflection}] *}
 
 text {*
   Printing then out the components of the simpset gives:
 
   @{ML_response_fake [display,gray]
-  "print_ss @{context} ss1"
+  "print_ss @{context} (Raw_Simplifier.simpset_of ss1)"
 "Simplification rules:
   ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
 Congruences rules:
@@ -1484,13 +1486,13 @@
   Adding also the congruence rule @{thm [source] UN_cong} 
 *}
 
-ML %grayML{*val ss2 = Simplifier.add_cong (@{thm UN_cong} RS @{thm eq_reflection}) ss1 *}
+ML %grayML{*val ss2 = ss1 |> Simplifier.add_cong (@{thm UN_cong} RS @{thm eq_reflection}) *}
 
 text {*
   gives
 
   @{ML_response_fake [display,gray]
-  "print_ss @{context} ss2"
+  "print_ss @{context} (Raw_Simplifier.simpset_of ss2)"
 "Simplification rules:
   ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
 Congruences rules:
@@ -1528,7 +1530,7 @@
   and  "t \<equiv> t" 
   and  "False \<Longrightarrow> Foo" 
   and  "\<lbrakk>A; B; C\<rbrakk> \<Longrightarrow> A"
-apply(tactic {* ALLGOALS (simp_tac HOL_basic_ss) *})
+apply(tactic {* ALLGOALS (simp_tac (put_simpset HOL_basic_ss @{context})) *})
 done
 
 text {*
@@ -1711,17 +1713,18 @@
   the definition of the auxiliary constant. 
 *}
 
-ML %linenosgray{*val perm_simp_tac =
+ML %linenosgray{*fun perm_simp_tac ctxt =
 let
   val thms1 = [@{thm perm_aux_expand}]
   val thms2 = [@{thm perm_append}, @{thm perm_bij}, @{thm perm_rev}, 
                @{thm perm_compose_aux}] @ @{thms perm_prod.simps} @ 
                @{thms perm_list.simps} @ @{thms perm_nat.simps}
   val thms3 = [@{thm perm_aux_def}]
+  val ss = put_simpset HOL_basic_ss ctxt
 in
-  simp_tac (HOL_basic_ss addsimps thms1)
-  THEN' simp_tac (HOL_basic_ss addsimps thms2)
-  THEN' simp_tac (HOL_basic_ss addsimps thms3)
+  simp_tac (ss addsimps thms1)
+  THEN' simp_tac (ss addsimps thms2)
+  THEN' simp_tac (ss addsimps thms3)
 end*}
 
 text {*
@@ -1733,7 +1736,7 @@
 lemma 
   fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
   shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
-apply(tactic {* perm_simp_tac 1 *})
+apply(tactic {* perm_simp_tac @{context} 1 *})
 done
 
 
@@ -1749,8 +1752,6 @@
   (FIXME: What are the second components of the congruence rules---something to
   do with weak congruence constants?)
 
-  (FIXME: Anything interesting to say about @{ML Simplifier.clear_ss}?)
-
   (FIXME: what are @{ML mksimps_pairs}; used in Nominal.thy)
 
   (FIXME: explain @{ML simplify} and @{ML "Simplifier.rewrite_rule"} etc.)
@@ -1771,9 +1772,8 @@
   you can use the function:
 *}
 
-ML %linenosgray{*fun fail_simproc simpset redex = 
+ML %linenosgray{*fun fail_simproc ctxt redex = 
 let
-  val ctxt = Simplifier.the_context simpset
   val _ = pwriteln (Pretty.block 
     [Pretty.str "The redex: ", pretty_cterm ctxt redex])
 in
@@ -1830,7 +1830,8 @@
 
 lemma 
   shows "Suc 0 = 1"
-apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc fail}]) 1*})
+apply(tactic {* simp_tac (put_simpset 
+  HOL_basic_ss @{context} addsimprocs [@{simproc fail}]) 1*})
 (*<*)oops(*>*)
 
 text {*
@@ -1844,9 +1845,8 @@
   to
 *}
 
-ML %grayML{*fun fail_simproc' simpset redex = 
+ML %grayML{*fun fail_simproc' ctxt redex = 
 let
-  val ctxt = Simplifier.the_context simpset
   val _ = pwriteln (Pretty.block 
     [Pretty.str "The redex:", pretty_term ctxt redex])
 in
@@ -1861,12 +1861,12 @@
 *}
 
 
-ML %grayML{*val fail' = 
+ML %grayML{*fun fail' ctxt = 
 let 
   val thy = @{theory}
   val pat = [@{term "Suc n"}]
 in
-  Simplifier.simproc_global_i thy "fail_simproc'" pat (K fail_simproc')
+  Simplifier.simproc_global_i thy "fail_simproc'" pat (K fail_simproc' ctxt)
 end*}
 
 text {*
@@ -1882,7 +1882,7 @@
 
 lemma 
   shows "Suc (Suc 0) = (Suc 1)"
-apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [fail']) 1*})
+apply(tactic {* simp_tac ((put_simpset HOL_basic_ss @{context}) addsimprocs [fail' @{context}]) 1*})
 (*<*)oops(*>*)
 
 text {*
@@ -1909,7 +1909,7 @@
 *}
 
 
-ML %grayML{*fun plus_one_simproc ss redex =
+ML %grayML{*fun plus_one_simproc ctxt redex =
   case redex of
     @{term "Suc 0"} => NONE
   | _ => SOME @{thm plus_one}*}
@@ -1918,12 +1918,12 @@
   and set up the simproc as follows.
 *}
 
-ML %grayML{*val plus_one =
+ML %grayML{*fun plus_one ctxt =
 let
   val thy = @{theory}
   val pat = [@{term "Suc n"}] 
 in
-  Simplifier.simproc_global_i thy "sproc +1" pat (K plus_one_simproc)
+  Simplifier.simproc_global_i thy "sproc +1" pat (K plus_one_simproc ctxt)
 end*}
 
 text {*
@@ -1935,7 +1935,7 @@
 
 lemma 
   shows "P (Suc (Suc (Suc 0))) (Suc 0)"
-apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [plus_one]) 1*})
+apply(tactic {* simp_tac (put_simpset HOL_basic_ss @{context} addsimprocs [plus_one @{context}]) 1*})
 txt{*
   where the simproc produces the goal state
   \begin{isabelle}
@@ -1990,7 +1990,7 @@
 let
   val num = HOLogic.mk_number @{typ "nat"} n
   val goal = Logic.mk_equals (t, num)
-  val num_ss = HOL_ss addsimps @{thms semiring_norm}
+  val num_ss = put_simpset HOL_ss ctxt addsimps @{thms semiring_norm}
 in
   Goal.prove ctxt [] [] goal (K (simp_tac num_ss 1))
 end*}
@@ -2010,13 +2010,9 @@
   theorem for the simproc.
 *}
 
-ML %grayML{*fun nat_number_simproc ss t =
-let 
-  val ctxt = Simplifier.the_context ss
-in
+ML %grayML{*fun nat_number_simproc ctxt t =
   SOME (get_thm_alt ctxt (t, dest_suc_trm t))
-  handle TERM _ => NONE
-end*}
+  handle TERM _ => NONE *}
 
 text {*
   This function uses the fact that @{ML dest_suc_trm} might raise an exception 
@@ -2025,12 +2021,12 @@
   on an example, you can set it up as follows:
 *}
 
-ML %grayML{*val nat_number =
+ML %grayML{*fun nat_number ctxt =
 let
   val thy = @{theory}
   val pat = [@{term "Suc n"}]
 in 
-  Simplifier.simproc_global_i thy "nat_number" pat (K nat_number_simproc) 
+  Simplifier.simproc_global_i thy "nat_number" pat (K nat_number_simproc ctxt) 
 end*}
 
 text {* 
@@ -2039,7 +2035,7 @@
 
 lemma 
   shows "P (Suc (Suc 2)) (Suc 99) (0::nat) (Suc 4 + Suc 0) (Suc (0 + 0))"
-apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number]) 1*})
+apply(tactic {* simp_tac (put_simpset HOL_ss @{context} addsimprocs [nat_number @{context}]) 1*})
 txt {* 
   you obtain the more legible goal state
   \begin{isabelle}