--- 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);