diff -r f76fb8858e0b -r 54c0d4128b30 src/Tools/eqsubst.ML
--- a/src/Tools/eqsubst.ML	Thu May 30 17:21:11 2013 +0200
+++ b/src/Tools/eqsubst.ML	Thu May 30 17:26:01 2013 +0200
@@ -56,6 +56,10 @@
 fun prep_meta_eq ctxt =
   Simplifier.mksimps ctxt #> map Drule.zero_var_indexes;
 
+(* make free vars into schematic vars with index zero *)
+fun unfix_frees frees =
+   fold (K (Thm.forall_elim_var 0)) frees o Drule.forall_intr_list frees;
+
 
 type match =
   ((indexname * (sort * typ)) list (* type instantiations *)
@@ -246,7 +250,7 @@
 (* rule is the equation for substitution *)
 fun apply_subst_in_concl ctxt i st (cfvs, conclthm) rule m =
   RW_Inst.rw ctxt m rule conclthm
-  |> IsaND.unfix_frees cfvs
+  |> unfix_frees cfvs
   |> Conv.fconv_rule Drule.beta_eta_conversion
   |> (fn r => Tactic.rtac r i st);
 
@@ -326,7 +330,7 @@
       RW_Inst.rw ctxt m rule pth
       |> (Seq.hd o prune_params_tac)
       |> Thm.permute_prems 0 ~1 (* put old asm first *)
-      |> IsaND.unfix_frees cfvs (* unfix any global params *)
+      |> unfix_frees cfvs (* unfix any global params *)
       |> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *)
   in
     (* ~j because new asm starts at back, thus we subtract 1 *)