src/Pure/codegen.ML
changeset 33957 e9afca2118d4
parent 33955 fff6f11b1f09
child 35232 f588e1169c8b
--- a/src/Pure/codegen.ML	Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Pure/codegen.ML	Wed Nov 25 09:13:46 2009 +0100
@@ -579,11 +579,11 @@
 fun eta_expand t ts i =
   let
     val k = length ts;
-    val Ts = (uncurry drop) (k, binder_types (fastype_of t));
+    val Ts = drop k (binder_types (fastype_of t));
     val j = i - k
   in
     List.foldr (fn (T, t) => Abs ("x", T, t))
-      (list_comb (t, ts @ map Bound (j-1 downto 0))) ((uncurry take) (j, Ts))
+      (list_comb (t, ts @ map Bound (j-1 downto 0))) (take j Ts)
   end;
 
 fun mk_app _ p [] = p