src/HOL/Nominal/nominal_fresh_fun.ML
changeset 59058 a78612c67ec0
parent 58956 a816aa3ff391
child 59582 0fbed69ff081
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Nov 26 16:55:43 2014 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Nov 26 20:05:34 2014 +0100
     1.3 @@ -23,8 +23,8 @@
     1.4        (head_of (Logic.incr_indexes (Ts, j) t),
     1.5         fold_rev Term.abs ps u)) tinst;
     1.6      val th' = instf
     1.7 -      (map (pairself (ctyp_of thy)) tyinst')
     1.8 -      (map (pairself (cterm_of thy)) tinst')
     1.9 +      (map (apply2 (ctyp_of thy)) tyinst')
    1.10 +      (map (apply2 (cterm_of thy)) tinst')
    1.11        (Thm.lift_rule cgoal th)
    1.12    in
    1.13      compose_tac ctxt (elim, th', nprems_of th) i st