diff -r 894e82be8d05 -r af4c18c30593 src/HOL/Bali/AxExample.thy
--- a/src/HOL/Bali/AxExample.thy	Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/AxExample.thy	Wed Feb 10 00:45:16 2010 +0100
@@ -166,7 +166,7 @@
 apply  (tactic "ax_tac 1" (* NewC *))
 apply  (tactic "ax_tac 1" (* ax_Alloc *))
      (* just for clarification: *)
-apply  (rule_tac Q' = "Normal ((\<lambda>Y s Z. arr_inv (store s) \<and> vf=lvar (VName e) (store s)) \<and>. heap_free tree \<and>. initd Ext)" in conseq2)
+apply  (rule_tac Q' = "Normal ((\<lambda>Y s Z. arr_inv (store s) \<and> vf=lvar (VName e) (store s)) \<and>. heap_free three \<and>. initd Ext)" in conseq2)
 prefer 2
 apply   (simp add: invocation_declclass_def dynmethd_def)
 apply   (unfold dynlookup_def)