src/Tools/eqsubst.ML
changeset 52240 066c2ff17f7c
parent 52239 6a6033fa507c
child 52242 2d634bfa1bbf
     1.1 --- a/src/Tools/eqsubst.ML	Thu May 30 16:11:14 2013 +0200
     1.2 +++ b/src/Tools/eqsubst.ML	Thu May 30 16:31:53 2013 +0200
     1.3 @@ -123,7 +123,7 @@
     1.4  (* before matching we need to fake the bound vars that are missing an
     1.5     abstraction. In this function we additionally construct the
     1.6     abstraction environment, and an outer context term (with the focus
     1.7 -   abstracted out) for use in rewriting with RWInst.rw *)
     1.8 +   abstracted out) for use in rewriting with RW_Inst.rw *)
     1.9  fun prep_zipper_match z =
    1.10    let
    1.11      val t = Zipper.trm z
    1.12 @@ -245,7 +245,7 @@
    1.13  (* m is instantiation/match information *)
    1.14  (* rule is the equation for substitution *)
    1.15  fun apply_subst_in_concl ctxt i st (cfvs, conclthm) rule m =
    1.16 -  RWInst.rw ctxt m rule conclthm
    1.17 +  RW_Inst.rw ctxt m rule conclthm
    1.18    |> IsaND.unfix_frees cfvs
    1.19    |> Conv.fconv_rule Drule.beta_eta_conversion
    1.20    |> (fn r => Tactic.rtac r i st);
    1.21 @@ -323,7 +323,7 @@
    1.22    let
    1.23      val st2 = Thm.rotate_rule (j - 1) i st; (* put premice first *)
    1.24      val preelimrule =
    1.25 -      RWInst.rw ctxt m rule pth
    1.26 +      RW_Inst.rw ctxt m rule pth
    1.27        |> (Seq.hd o prune_params_tac)
    1.28        |> Thm.permute_prems 0 ~1 (* put old asm first *)
    1.29        |> IsaND.unfix_frees cfvs (* unfix any global params *)