--- a/src/HOL/Bali/AxExample.thy Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Bali/AxExample.thy Wed Mar 19 22:50:42 2008 +0100
@@ -136,7 +136,7 @@
apply (rule ax_subst_Var_allI)
apply (tactic {* inst1_tac "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"]) 1 *})
+apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [thm "peek_and_def2"]) 1 *})
apply (rule ax_derivs.Abrupt)
apply (simp (no_asm))
apply (tactic "ax_tac 1" (* FVar *))
@@ -186,26 +186,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 (@{simpset} 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 (@{simpset} 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 (@{simpset} 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 "P'" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
-apply (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [split_paired_All, thm "peek_and_def2"]) 2 *})
+apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [split_paired_All, thm "peek_and_def2"]) 2 *})
apply (tactic "ax_tac 2" (* NewA *))
apply (tactic "ax_tac 3" (* ax_Alloc_Arr *))
apply (tactic "ax_tac 3")
apply (tactic {* inst1_tac "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 (@{simpset} delloop "split_all_tac") 2 *})
apply (tactic "ax_tac 2")
apply (tactic "ax_tac 1" (* FVar *))
apply (tactic "ax_tac 2" (* StatRef *))
@@ -216,7 +216,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 (@{simpset} delloop "split_all_tac") 1 *})
apply (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])
apply (rule wf_tprg)
apply clarsimp