--- a/src/HOL/Bali/AxExample.thy Wed May 26 16:17:30 2010 +0200
+++ b/src/HOL/Bali/AxExample.thy Wed May 26 16:28:55 2010 +0200
@@ -189,7 +189,7 @@
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 [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 (@{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 "ax_tac 2" (* NewA *))
apply (tactic "ax_tac 3" (* ax_Alloc_Arr *))
apply (tactic "ax_tac 3")