diff -r 340df9f3491f -r 22f665a2e91c src/HOL/Bali/AxExample.thy
--- a/src/HOL/Bali/AxExample.thy	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Bali/AxExample.thy	Mon Sep 12 07:55:43 2011 +0200
@@ -133,7 +133,7 @@
 apply       (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2")
 apply      (tactic "ax_tac 1")
 apply     (tactic {* inst1_tac @{context} "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
+apply     fastforce
 prefer 4
 apply    (rule ax_derivs.Done [THEN conseq1],force)
 apply   (rule ax_subst_Val_allI)