src/HOL/Bali/AxExample.thy

 apply      (tactic "ax_tac 1") (* Ass *)
 prefer 2
 apply       (rule ax_subst_Var_allI)
 apply       (tactic {* inst1_tac @{context} "P'" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *})
 apply       (rule allI)
-apply       (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [@{thm peek_and_def2}, @{thm heap_def2}, @{thm subst_res_def2}, @{thm normal_def2}]) 1 *})
+apply       (tactic {* simp_tac (@{context} delloop "split_all_tac" delsimps [@{thm peek_and_def2}, @{thm heap_def2}, @{thm subst_res_def2}, @{thm normal_def2}]) 1 *})
 apply       (rule ax_derivs.Abrupt)
 apply      (simp (no_asm))
 apply      (tactic "ax_tac 1" (* FVar *))
 apply       (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2")
 apply      (tactic "ax_tac 1")

 apply   (force elim!: arr_inv_new_obj atleast_free_SucD atleast_free_weaken)
      (* begin init *)
 apply  (rule ax_InitS)
 apply     force
 apply    (simp (no_asm))
-apply   (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 1 *})
+apply   (tactic {* simp_tac (@{context} delloop "split_all_tac") 1 *})
 apply   (rule ax_Init_Skip_lemma)
-apply  (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 1 *})
+apply  (tactic {* simp_tac (@{context} delloop "split_all_tac") 1 *})
 apply  (rule ax_InitS [THEN conseq1] (* init Base *))
 apply      force
 apply     (simp (no_asm))
 apply    (unfold arr_viewed_from_def)
 apply    (rule allI)
 apply    (rule_tac P' = "Normal ?P" in conseq1)
-apply     (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 1 *})
+apply     (tactic {* simp_tac (@{context} delloop "split_all_tac") 1 *})
 apply     (tactic "ax_tac 1")
 apply     (tactic "ax_tac 1")
 apply     (rule_tac [2] ax_subst_Var_allI)
 apply      (tactic {* inst1_tac @{context} "P'" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
-apply     (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [@{thm split_paired_All}, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2 *})
+apply     (tactic {* simp_tac (@{context} delloop "split_all_tac" delsimps [@{thm split_paired_All}, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2 *})
 apply      (tactic "ax_tac 2" (* NewA *))
 apply       (tactic "ax_tac 3" (* ax_Alloc_Arr *))
 apply       (tactic "ax_tac 3")
 apply      (tactic {* inst1_tac @{context} "P" "\<lambda>vf l vfa. Normal (?P vf l vfa\<leftarrow>\<diamondsuit>)" *})
-apply      (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 2 *})
+apply      (tactic {* simp_tac (@{context} delloop "split_all_tac") 2 *})
 apply      (tactic "ax_tac 2")
 apply     (tactic "ax_tac 1" (* FVar *))
 apply      (tactic "ax_tac 2" (* StatRef *))
 apply     (rule ax_derivs.Done [THEN conseq1])
 apply     (tactic {* inst1_tac @{context} "Q" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Base \<and>. initd Ext)" *})
 apply     (clarsimp split del: split_if)
 apply     (frule atleast_free_weaken [THEN atleast_free_weaken])
 apply     (drule initedD)
 apply     (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def)
 apply    force
-apply   (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 1 *})
+apply   (tactic {* simp_tac (@{context} delloop "split_all_tac") 1 *})
 apply   (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])
 apply     (rule wf_tprg)
 apply    clarsimp
 apply   (tactic {* inst1_tac @{context} "P" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" *})
 apply   clarsimp