src/Tools/eqsubst.ML
changeset 52239 6a6033fa507c
parent 52238 d84ff5a93764
child 52240 066c2ff17f7c
     1.1 --- a/src/Tools/eqsubst.ML	Thu May 30 15:51:55 2013 +0200
     1.2 +++ b/src/Tools/eqsubst.ML	Thu May 30 16:11:14 2013 +0200
     1.3 @@ -247,7 +247,7 @@
     1.4  fun apply_subst_in_concl ctxt i st (cfvs, conclthm) rule m =
     1.5    RWInst.rw ctxt m rule conclthm
     1.6    |> IsaND.unfix_frees cfvs
     1.7 -  |> RWInst.beta_eta_contract
     1.8 +  |> Conv.fconv_rule Drule.beta_eta_conversion
     1.9    |> (fn r => Tactic.rtac r i st);
    1.10  
    1.11  (* substitute within the conclusion of goal i of gth, using a meta
    1.12 @@ -327,7 +327,7 @@
    1.13        |> (Seq.hd o prune_params_tac)
    1.14        |> Thm.permute_prems 0 ~1 (* put old asm first *)
    1.15        |> IsaND.unfix_frees cfvs (* unfix any global params *)
    1.16 -      |> RWInst.beta_eta_contract; (* normal form *)
    1.17 +      |> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *)
    1.18    in
    1.19      (* ~j because new asm starts at back, thus we subtract 1 *)
    1.20      Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i))