diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Bali/AxExample.thy
--- a/src/HOL/Bali/AxExample.thy	Sat Jul 18 20:53:05 2015 +0200
+++ b/src/HOL/Bali/AxExample.thy	Sat Jul 18 20:54:56 2015 +0200
@@ -47,7 +47,7 @@
   | NONE => Seq.empty);
 
 fun ax_tac ctxt =
-  REPEAT o rtac allI THEN'
+  REPEAT o resolve_tac ctxt [allI] THEN'
   resolve_tac ctxt
     @{thms ax_Skip ax_StatRef ax_MethdN ax_Alloc ax_Alloc_Arr ax_SXAlloc_Normal ax_derivs.intros(8-)};
 *}