diff -r e9b7e210ad2a -r acfdd493f5c4 src/HOL/Bali/AxExample.thy
--- a/src/HOL/Bali/AxExample.thy	Thu Apr 21 17:22:23 2005 +0200
+++ b/src/HOL/Bali/AxExample.thy	Thu Apr 21 18:56:03 2005 +0200
@@ -39,8 +39,9 @@
 declare split_if_asm [split del]
 declare lvar_def [simp]
 
-ML {*
-fun inst1_tac s t = instantiate_tac [(s,t)];
+ML_setup {*
+fun inst1_tac s t st = case assoc (rev (term_varnames (prop_of st)), s) of
+  SOME i => Tactic.instantiate_tac' [((s, i), t)] st | NONE => Seq.empty;
 val ax_tac = REPEAT o rtac allI THEN'
              resolve_tac(thm "ax_Skip"::thm "ax_StatRef"::thm "ax_MethdN"::
                          thm "ax_Alloc"::thm "ax_Alloc_Arr"::
@@ -60,7 +61,7 @@
          precondition. *)
 apply  (tactic "ax_tac 1" (* Try *))
 defer
-apply    (tactic {* inst1_tac "Q1" 
+apply    (tactic {* inst1_tac "Q" 
                  "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" *})
 prefer 2
 apply    simp
@@ -80,7 +81,7 @@
 apply   (tactic "ax_tac 1" (* AVar *))
 prefer 2
 apply    (rule ax_subst_Val_allI)
-apply    (tactic {* inst1_tac "P'21" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
+apply    (tactic {* inst1_tac "P'" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
 apply    (simp del: avar_def2 peek_and_def2)
 apply    (tactic "ax_tac 1")
 apply   (tactic "ax_tac 1")
@@ -121,7 +122,7 @@
 apply      (tactic "ax_tac 1") (* Ass *)
 prefer 2
 apply       (rule ax_subst_Var_allI)
-apply       (tactic {* inst1_tac "P'29" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *})
+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       (rule ax_derivs.Abrupt)
@@ -129,17 +130,17 @@
 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     (tactic {* inst1_tac "R14" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> vs = [Null]) \<and>. heap_free two)" *})
+apply     (tactic {* inst1_tac "R" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> vs = [Null]) \<and>. heap_free two)" *})
 apply     fastsimp
 prefer 4
 apply    (rule ax_derivs.Done [THEN conseq1],force)
 apply   (rule ax_subst_Val_allI)
-apply   (tactic {* inst1_tac "P'34" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
+apply   (tactic {* inst1_tac "P'" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
 apply   (simp (no_asm) del: peek_and_def2)
 apply   (tactic "ax_tac 1")
 prefer 2
 apply   (rule ax_subst_Val_allI)
-apply    (tactic {* inst1_tac "P'4" "\<lambda>aa v. Normal (?QQ aa v\<leftarrow>?y)" *})
+apply    (tactic {* inst1_tac "P'" "\<lambda>aa v. Normal (?QQ aa v\<leftarrow>?y)" *})
 apply    (simp del: peek_and_def2)
 apply    (tactic "ax_tac 1")
 apply   (tactic "ax_tac 1")
@@ -158,7 +159,7 @@
 apply (tactic "ax_tac 1")
 defer
 apply  (rule ax_subst_Var_allI)
-apply  (tactic {* inst1_tac "P'14" "\<lambda>u vf. Normal (?PP vf \<and>. ?p) u" *})
+apply  (tactic {* inst1_tac "P'" "\<lambda>u vf. Normal (?PP vf \<and>. ?p) u" *})
 apply  (simp (no_asm) del: split_paired_All peek_and_def2)
 apply  (tactic "ax_tac 1" (* NewC *))
 apply  (tactic "ax_tac 1" (* ax_Alloc *))
@@ -186,7 +187,7 @@
 apply     (tactic "ax_tac 1")
 apply     (tactic "ax_tac 1")
 apply     (rule_tac [2] ax_subst_Var_allI)
-apply      (tactic {* inst1_tac "P'29" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
+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 "ax_tac 2" (* NewA *))
 apply       (tactic "ax_tac 3" (* ax_Alloc_Arr *))
@@ -197,7 +198,7 @@
 apply     (tactic "ax_tac 1" (* FVar *))
 apply      (tactic "ax_tac 2" (* StatRef *))
 apply     (rule ax_derivs.Done [THEN conseq1])
-apply     (tactic {* inst1_tac "Q22" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Base \<and>. initd Ext)" *})
+apply     (tactic {* inst1_tac "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)
@@ -207,7 +208,7 @@
 apply   (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])
 apply     (rule wf_tprg)
 apply    clarsimp
-apply   (tactic {* inst1_tac "P22" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" *})
+apply   (tactic {* inst1_tac "P" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" *})
 apply   clarsimp
 apply  (tactic {* inst1_tac "PP" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. Not \<circ> initd Base)" *})
 apply  clarsimp
@@ -241,7 +242,7 @@
 apply  clarsimp
 apply (tactic "ax_tac 1" (* If *))
 apply  (tactic 
-  {* inst1_tac "P'21" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" *})
+  {* inst1_tac "P'" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" *})
 apply  (tactic "ax_tac 1")
 apply  (rule conseq1)
 apply   (tactic "ax_tac 1")
@@ -262,7 +263,7 @@
 apply  (tactic "ax_tac 1")
 prefer 2
 apply   (rule ax_subst_Var_allI)
-apply   (tactic {* inst1_tac "P'29" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" *})
+apply   (tactic {* inst1_tac "P'" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" *})
 apply   (rule allI)
 apply   (rule_tac P' = "Normal ?P" in conseq1)
 prefer 2