src/Tools/eqsubst.ML
changeset 52732 b4da1f2ec73f
parent 52246 54c0d4128b30
child 53168 d998de7f0efc
     1.1 --- a/src/Tools/eqsubst.ML	Thu Jul 25 16:46:53 2013 +0200
     1.2 +++ b/src/Tools/eqsubst.ML	Sat Jul 27 16:35:51 2013 +0200
     1.3 @@ -252,7 +252,7 @@
     1.4    RW_Inst.rw ctxt m rule conclthm
     1.5    |> unfix_frees cfvs
     1.6    |> Conv.fconv_rule Drule.beta_eta_conversion
     1.7 -  |> (fn r => Tactic.rtac r i st);
     1.8 +  |> (fn r => rtac r i st);
     1.9  
    1.10  (* substitute within the conclusion of goal i of gth, using a meta
    1.11  equation rule. Note that we assume rule has var indicies zero'd *)
    1.12 @@ -334,8 +334,7 @@
    1.13        |> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *)
    1.14    in
    1.15      (* ~j because new asm starts at back, thus we subtract 1 *)
    1.16 -    Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i))
    1.17 -      (Tactic.dtac preelimrule i st2)
    1.18 +    Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i)) (dtac preelimrule i st2)
    1.19    end;
    1.20  
    1.21