Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Nominal/nominal_fresh_fun.ML
changeset 59058 a78612c67ec0
parent 58956 a816aa3ff391
child 59582 0fbed69ff081 
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Nov 26 16:55:43 2014 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Nov 26 20:05:34 2014 +0100
@@ -23,8 +23,8 @@
       (head_of (Logic.incr_indexes (Ts, j) t),
        fold_rev Term.abs ps u)) tinst;
     val th' = instf
-      (map (pairself (ctyp_of thy)) tyinst')
-      (map (pairself (cterm_of thy)) tinst')
+      (map (apply2 (ctyp_of thy)) tyinst')
+      (map (apply2 (cterm_of thy)) tinst')
       (Thm.lift_rule cgoal th)
   in
     compose_tac ctxt (elim, th', nprems_of th) i st
isabelle