src/Tools/eqsubst.ML
changeset 52246 54c0d4128b30
parent 52242 2d634bfa1bbf
child 52732 b4da1f2ec73f
     1.1 --- a/src/Tools/eqsubst.ML	Thu May 30 17:21:11 2013 +0200
     1.2 +++ b/src/Tools/eqsubst.ML	Thu May 30 17:26:01 2013 +0200
     1.3 @@ -56,6 +56,10 @@
     1.4  fun prep_meta_eq ctxt =
     1.5    Simplifier.mksimps ctxt #> map Drule.zero_var_indexes;
     1.6  
     1.7 +(* make free vars into schematic vars with index zero *)
     1.8 +fun unfix_frees frees =
     1.9 +   fold (K (Thm.forall_elim_var 0)) frees o Drule.forall_intr_list frees;
    1.10 +
    1.11  
    1.12  type match =
    1.13    ((indexname * (sort * typ)) list (* type instantiations *)
    1.14 @@ -246,7 +250,7 @@
    1.15  (* rule is the equation for substitution *)
    1.16  fun apply_subst_in_concl ctxt i st (cfvs, conclthm) rule m =
    1.17    RW_Inst.rw ctxt m rule conclthm
    1.18 -  |> IsaND.unfix_frees cfvs
    1.19 +  |> unfix_frees cfvs
    1.20    |> Conv.fconv_rule Drule.beta_eta_conversion
    1.21    |> (fn r => Tactic.rtac r i st);
    1.22  
    1.23 @@ -326,7 +330,7 @@
    1.24        RW_Inst.rw ctxt m rule pth
    1.25        |> (Seq.hd o prune_params_tac)
    1.26        |> Thm.permute_prems 0 ~1 (* put old asm first *)
    1.27 -      |> IsaND.unfix_frees cfvs (* unfix any global params *)
    1.28 +      |> unfix_frees cfvs (* unfix any global params *)
    1.29        |> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *)
    1.30    in
    1.31      (* ~j because new asm starts at back, thus we subtract 1 *)