src/HOL/Bali/AxExample.thy

--- a/src/HOL/Bali/AxExample.thy	Thu Mar 19 17:25:57 2015 +0100
+++ b/src/HOL/Bali/AxExample.thy	Thu Mar 19 22:30:57 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), t)] xs st
+    SOME i => Rule_Insts.instantiate_tac ctxt [(((s, i), Position.none), t)] xs st
   | NONE => Seq.empty);
 
 fun ax_tac ctxt =