src/Tools/eqsubst.ML

 struct
 
 (* changes object "=" to meta "==" which prepares a given rewrite rule *)
 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 *)
    * (indexname * (typ * term)) list) (* term instantiations *)

 (* conclthm is a theorem of for just the conclusion *)
 (* m is instantiation/match information *)
 (* 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);
 
 (* substitute within the conclusion of goal i of gth, using a meta
 equation rule. Note that we assume rule has var indicies zero'd *)

     val st2 = Thm.rotate_rule (j - 1) i st; (* put premice first *)
     val preelimrule =
       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 *)
     Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i))
       (Tactic.dtac preelimrule i st2)