--- a/src/HOL/Bali/AxExample.thy Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/Bali/AxExample.thy Thu Apr 18 17:07:01 2013 +0200
@@ -126,7 +126,7 @@
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 *))
@@ -176,26 +176,26 @@
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 *))
@@ -206,7 +206,7 @@
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