diff -r 27509e72f29e -r 63e0ab9f2ea9 src/HOL/Bali/AxExample.thy
--- a/src/HOL/Bali/AxExample.thy	Wed Sep 14 01:47:06 2005 +0200
+++ b/src/HOL/Bali/AxExample.thy	Wed Sep 14 10:13:12 2005 +0200
@@ -40,7 +40,7 @@
 declare lvar_def [simp]
 
 ML {*
-fun inst1_tac s t st = case assoc (rev (term_varnames (prop_of st)), s) of
+fun inst1_tac s t st = case AList.lookup (op =) (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'
              resolve_tac(thm "ax_Skip"::thm "ax_StatRef"::thm "ax_MethdN"::