src/Tools/eqsubst.ML
changeset 54742 7a86358a3c0b
parent 53168 d998de7f0efc
child 58318 f95754ca7082
     1.1 --- a/src/Tools/eqsubst.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/Tools/eqsubst.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -328,7 +328,7 @@
     1.4      val st2 = Thm.rotate_rule (j - 1) i st; (* put premice first *)
     1.5      val preelimrule =
     1.6        RW_Inst.rw ctxt m rule pth
     1.7 -      |> (Seq.hd o prune_params_tac)
     1.8 +      |> (Seq.hd o prune_params_tac ctxt)
     1.9        |> Thm.permute_prems 0 ~1 (* put old asm first *)
    1.10        |> unfix_frees cfvs (* unfix any global params *)
    1.11        |> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *)