# HG changeset patch
# User wenzelm
# Date 1369407844 -7200
# Node ID fa9e563f6bcf0ac225beb5207873bd408d3f915f
# Parent  366fa32ee2a361184e47fb1de4918e48e315bda3
tuned;

diff -r 366fa32ee2a3 -r fa9e563f6bcf src/Pure/envir.ML
--- a/src/Pure/envir.ML	Fri May 24 17:00:46 2013 +0200
+++ b/src/Pure/envir.ML	Fri May 24 17:04:04 2013 +0200
@@ -254,10 +254,11 @@
           let
             val Us = binder_types (fastype_of1 (Ts, t));
             val i = length Us;
+            val long = eta_long (rev Us @ Ts);
           in
             fold_rev (Term.abs o pair "x") Us
-              (list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts))
-                (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0))))
+              (list_comb (incr_boundvars i u,
+                map (long o incr_boundvars i) ts @ map (long o Bound) (i - 1 downto 0)))
           end);