--- a/src/HOL/Bali/AxExample.thy Sat Jan 25 23:50:49 2014 +0100
+++ b/src/HOL/Bali/AxExample.thy Sun Jan 26 13:45:40 2014 +0100
@@ -42,8 +42,9 @@
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 => instantiate_tac ctxt [((s, i), t)] xs st | NONE => Seq.empty;
+ (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
+ | NONE => Seq.empty);
val ax_tac =
REPEAT o rtac allI THEN'