src/Tools/eqsubst.ML
changeset 59498 50b60f501b05
parent 58950 d07464875dd4
child 59621 291934bac95e
     1.1 --- a/src/Tools/eqsubst.ML	Tue Feb 10 14:29:36 2015 +0100
     1.2 +++ b/src/Tools/eqsubst.ML	Tue Feb 10 14:48:26 2015 +0100
     1.3 @@ -250,7 +250,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 => resolve_tac [r] i st);
     1.8 +  |> (fn r => resolve_tac ctxt [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 @@ -332,7 +332,8 @@
    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)) (dresolve_tac [preelimrule] i st2)
    1.17 +    Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i))
    1.18 +      (dresolve_tac ctxt [preelimrule] i st2)
    1.19    end;
    1.20  
    1.21