--- a/ProgTutorial/Essential.thy	Fri Mar 01 00:49:15 2013 +0000
+++ b/ProgTutorial/Essential.thy	Fri Apr 19 11:09:18 2013 +0100
@@ -1605,7 +1605,7 @@
   "let
   fun pred s = match_string \"my_thm_simp\" s
 in
-  exists pred (get_thm_names_from_ss @{simpset})
+  exists pred (get_thm_names_from_ss @{context})
 end"
   "true"}
 
@@ -1899,7 +1899,7 @@
   \begin{readmore}
   Functions that setup goal states and prove theorems are implemented in 
   @{ML_file "Pure/goal.ML"}. A function and a tactic that allow one to
-  skip proofs of theorems are implemented in @{ML_file "Pure/Isar/skip_proof.ML"}.
+  skip proofs of theorems are implemented in @{ML_file "Pure/skip_proof.ML"}.
   \end{readmore}
 
   Theorems also contain auxiliary data, such as the name of the theorem, its

--- a/ProgTutorial/First_Steps.thy	Fri Mar 01 00:49:15 2013 +0000
+++ b/ProgTutorial/First_Steps.thy	Fri Apr 19 11:09:18 2013 +0100
@@ -842,8 +842,9 @@
   simpset.
 *}
 
-ML %grayML{*fun get_thm_names_from_ss simpset =
+ML %grayML{*fun get_thm_names_from_ss ctxt =
 let
+  val simpset = Raw_Simplifier.simpset_of ctxt
   val {simps,...} = Raw_Simplifier.dest_ss simpset
 in
   map #1 simps
@@ -853,10 +854,10 @@
   The function @{ML_ind dest_ss in Raw_Simplifier} returns a record containing all
   information stored in the simpset, but here we are only interested in the names of the
   simp-rules. Now you can feed in the current simpset into this function. 
-  The current simpset can be referred to using the antiquotation @{text "@{simpset}"}.
+  The current simpset can be referred to using @{ML_ind simpset_of in Raw_Simplifier}.
 
   @{ML_response_fake [display,gray] 
-  "get_thm_names_from_ss @{simpset}" 
+  "get_thm_names_from_ss @{context}" 
   "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
 
   Again, this way of referencing simpsets makes you independent from additions

--- a/ProgTutorial/Package/Ind_Extensions.thy	Fri Mar 01 00:49:15 2013 +0000
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Fri Apr 19 11:09:18 2013 +0100
@@ -193,7 +193,7 @@
 text {* Type declarations *}
 
 ML %grayML{*Typedef.add_typedef_global (@{binding test}, [], NoSyn)
-  @{term "{1}::nat set"} NONE (simp_tac @{simpset} 1) @{theory} *}
+  @{term "{1}::nat set"} NONE (simp_tac @{context} 1) @{theory} *}
 
 ML %grayML{*fun pat_completeness_auto ctxt =
   Pat_Completeness.pat_completeness_tac ctxt 1

--- a/ProgTutorial/Parsing.thy	Fri Mar 01 00:49:15 2013 +0000
+++ b/ProgTutorial/Parsing.thy	Fri Apr 19 11:09:18 2013 +0100
@@ -798,6 +798,7 @@
 
 section {* Parsing Specifications\label{sec:parsingspecs} *}
 
+
 text {*
   There are a number of special purpose parsers that help with parsing
   specifications of function definitions, inductive predicates and so on. In
@@ -1512,7 +1513,7 @@
 oops
 
 method_setup joker = {* 
-  Scan.lift (Scan.succeed (fn ctxt => Method.cheating true ctxt)) *} {* bla *}
+  Scan.lift (Scan.succeed (fn ctxt => Method.cheating true)) *} {* bla *}
 
 lemma "False"
 apply(joker)

--- a/ProgTutorial/Recipes/Timing.thy	Fri Mar 01 00:49:15 2013 +0000
+++ b/ProgTutorial/Recipes/Timing.thy	Fri Apr 19 11:09:18 2013 +0100
@@ -52,7 +52,7 @@
 
 lemma "ackermann (3, 4) = 125"
 apply(tactic {* 
-  timing_wrapper (simp_tac (@{simpset} addsimps @{thms "eval_nat_numeral"}) 1) *})
+  timing_wrapper (simp_tac (@{context} addsimps @{thms "eval_nat_numeral"}) 1) *})
 done
 
 text {*

--- a/ProgTutorial/Solutions.thy	Fri Mar 01 00:49:15 2013 +0000
+++ b/ProgTutorial/Solutions.thy	Fri Apr 19 11:09:18 2013 +0100
@@ -239,9 +239,8 @@
   Goal.prove ctxt [] [] goal (K (Arith_Data.arith_tac ctxt 1))
 end
 
-fun add_sp_aux ss t =
+fun add_sp_aux ctxt t =
 let 
-  val ctxt = Simplifier.the_context ss
   val t' = term_of t
 in
   SOME (get_sum_thm ctxt t' (dest_sum t'))
@@ -255,7 +254,7 @@
 text {* and a test case is the lemma *}
 
 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) ((4 + 1)::nat)"
-  apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]) 1 *})
+  apply(tactic {* simp_tac (put_simpset HOL_basic_ss @{context} addsimprocs [@{simproc add_sp}]) 1 *})
 txt {* 
   where the simproc produces the goal state
   
@@ -348,21 +347,23 @@
   then prove the remaining goal using @{ML "cheat_tac" in Skip_Proof}.
 *}
 
+ML Skip_Proof.cheat_tac
+
 ML %grayML{*local
   fun mk_tac tac = 
-        timing_wrapper (EVERY1 [tac, K (Skip_Proof.cheat_tac @{theory})])
+        timing_wrapper (EVERY1 [tac, Skip_Proof.cheat_tac])
 in
-  val c_tac = mk_tac (add_tac @{context}) 
-  val s_tac = mk_tac (simp_tac 
-                       (HOL_basic_ss addsimprocs [@{simproc add_sp}]))
+  fun c_tac ctxt = mk_tac (add_tac ctxt) 
+  fun s_tac ctxt = mk_tac (simp_tac 
+    (put_simpset HOL_basic_ss ctxt addsimprocs [@{simproc add_sp}]))
 end*}
 
 text {*
   This is all we need to let the conversion run against the simproc:
 *}
 
-ML %grayML{*val _ = Goal.prove @{context} [] [] (goal 8) (K c_tac)
-val _ = Goal.prove @{context} [] [] (goal 8) (K s_tac)*}
+ML %grayML{*val _ = Goal.prove @{context} [] [] (goal 8) (fn {context, ...} => c_tac context)
+val _ = Goal.prove @{context} [] [] (goal 8) (fn {context, ...} => s_tac context)*}
 
 text {*
   If you do the exercise, you can see that both ways of simplifying additions

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

Binary file progtutorial.pdf has changed