diff -r 6a449deff8d9 -r a80aa66d2271 src/HOL/Bali/AxExample.thy
--- a/src/HOL/Bali/AxExample.thy	Tue May 31 11:53:11 2005 +0200
+++ b/src/HOL/Bali/AxExample.thy	Tue May 31 11:53:12 2005 +0200
@@ -39,7 +39,7 @@
 declare split_if_asm [split del]
 declare lvar_def [simp]
 
-ML_setup {*
+ML {*
 fun inst1_tac s t st = case assoc (rev (term_varnames (prop_of st)), s) of
   SOME i => Tactic.instantiate_tac' [((s, i), t)] st | NONE => Seq.empty;
 val ax_tac = REPEAT o rtac allI THEN'