--- a/ProgTutorial/Solutions.thy	Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Solutions.thy	Tue May 14 11:10:53 2019 +0200
@@ -141,7 +141,7 @@
 text {* \solution{ex:dyckhoff} *}
 
 text {* 
-  The axiom rule can be implemented with the function @{ML atac}. The other
+  The axiom rule can be implemented with the function @{ML assume_tac}. The other
   rules correspond to the theorems:
 
   \begin{center}
@@ -182,26 +182,26 @@
   as follows.
 *}
 
-ML %linenosgray{*val apply_tac =
+ML %linenosgray{*fun apply_tac ctxt =
 let
   val intros = @{thms conjI disjI1 disjI2 impI iffI}
   val elims = @{thms FalseE conjE disjE iffE impE2}
 in
-  atac
-  ORELSE' resolve_tac intros
-  ORELSE' eresolve_tac elims
-  ORELSE' (etac @{thm impE1} THEN' atac)
+  assume_tac ctxt
+  ORELSE' resolve_tac ctxt intros
+  ORELSE' eresolve_tac ctxt elims
+  ORELSE' (eresolve_tac ctxt [@{thm impE1}] THEN' assume_tac ctxt)
 end*}
 
 text {*
   In Line 11 we apply the rule @{thm [source] impE1} in concjunction 
-  with @{ML atac} in order to reduce the number of possibilities that
+  with @{ML assume_tac} in order to reduce the number of possibilities that
   need to be explored. You can use the tactic as follows.
 *}
 
 lemma
   shows "((((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> Q) \<longrightarrow> Q"
-apply(tactic {* (DEPTH_SOLVE o apply_tac) 1 *})
+apply(tactic {* (DEPTH_SOLVE o apply_tac @{context}) 1 *})
 done
 
 text {*
@@ -214,7 +214,7 @@
   val goal = HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))
 in
   Goal.prove ctxt ["P"] [] goal
-   (fn _ => (DEPTH_SOLVE o apply_tac) 1)
+   (fn _ => (DEPTH_SOLVE o apply_tac ctxt) 1)
 end*}
 
 text {* 
@@ -227,7 +227,7 @@
 
 ML %grayML{*fun dest_sum term =
   case term of 
-    (@{term "(op +):: nat \<Rightarrow> nat \<Rightarrow> nat"} $ t1 $ t2) =>
+    (@{term "(+):: nat \<Rightarrow> nat \<Rightarrow> nat"} $ t1 $ t2) =>
         (snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2))
   | _ => raise TERM ("dest_sum", [term])
 
@@ -241,7 +241,7 @@
 
 fun add_sp_aux ctxt t =
 let 
-  val t' = term_of t
+  val t' = Thm.term_of t
 in
   SOME (get_sum_thm ctxt t' (dest_sum t'))
   handle TERM _ => NONE
@@ -275,7 +275,7 @@
   val trm = Thm.term_of ctrm
 in
   case trm of
-     @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => 
+     @{term "(+)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => 
         get_sum_thm ctxt trm (dest_sum trm)
     | _ => Conv.all_conv ctrm
 end
@@ -350,11 +350,11 @@
 ML Skip_Proof.cheat_tac
 
 ML %grayML{*local
-  fun mk_tac tac = 
-        timing_wrapper (EVERY1 [tac, Skip_Proof.cheat_tac])
+  fun mk_tac ctxt tac = 
+        timing_wrapper (EVERY1 [tac, Skip_Proof.cheat_tac ctxt])
 in
-  fun c_tac ctxt = mk_tac (add_tac ctxt) 
-  fun s_tac ctxt = mk_tac (simp_tac 
+  fun c_tac ctxt = mk_tac ctxt (add_tac ctxt) 
+  fun s_tac ctxt = mk_tac ctxt (simp_tac 
     (put_simpset HOL_basic_ss ctxt addsimprocs [@{simproc add_sp}]))
 end*}