tuned;

--- a/src/HOL/Bali/AxExample.thy	Fri Mar 20 11:48:34 2015 +0100
+++ b/src/HOL/Bali/AxExample.thy	Fri Mar 20 11:53:22 2015 +0100
@@ -48,8 +48,8 @@
 
 fun ax_tac ctxt =
   REPEAT o rtac allI THEN'
-  resolve_tac ctxt (@{thm ax_Skip} :: @{thm ax_StatRef} :: @{thm ax_MethdN} :: @{thm ax_Alloc} ::
-    @{thm ax_Alloc_Arr} :: @{thm ax_SXAlloc_Normal} :: @{thms ax_derivs.intros(8-)});
+  resolve_tac ctxt
+    @{thms ax_Skip ax_StatRef ax_MethdN ax_Alloc ax_Alloc_Arr ax_SXAlloc_Normal ax_derivs.intros(8-)};
 *}