diff -r a996f037c09d -r 558acf0426f1 src/HOL/Bali/AxExample.thy
--- a/src/HOL/Bali/AxExample.thy	Fri Mar 20 11:23:32 2015 +0100
+++ b/src/HOL/Bali/AxExample.thy	Fri Mar 20 11:48:34 2015 +0100
@@ -43,7 +43,7 @@
 ML {*
 fun inst1_tac ctxt s t xs st =
   (case AList.lookup (op =) (rev (Term.add_var_names (Thm.prop_of st) [])) s of
-    SOME i => Rule_Insts.instantiate_tac ctxt [(((s, i), Position.none), t)] xs st
+    SOME i => PRIMITIVE (Rule_Insts.read_instantiate ctxt [(((s, i), Position.none), t)] xs) st
   | NONE => Seq.empty);
 
 fun ax_tac ctxt =