--- 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)