src/Pure/codegen.ML
changeset 33955 fff6f11b1f09
parent 33522 737589bb9bb8
child 33957 e9afca2118d4
     1.1 --- a/src/Pure/codegen.ML	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/Pure/codegen.ML	Tue Nov 24 17:28:25 2009 +0100
     1.3 @@ -579,11 +579,11 @@
     1.4  fun eta_expand t ts i =
     1.5    let
     1.6      val k = length ts;
     1.7 -    val Ts = Library.drop (k, binder_types (fastype_of t));
     1.8 +    val Ts = (uncurry drop) (k, binder_types (fastype_of t));
     1.9      val j = i - k
    1.10    in
    1.11      List.foldr (fn (T, t) => Abs ("x", T, t))
    1.12 -      (list_comb (t, ts @ map Bound (j-1 downto 0))) (Library.take (j, Ts))
    1.13 +      (list_comb (t, ts @ map Bound (j-1 downto 0))) ((uncurry take) (j, Ts))
    1.14    end;
    1.15  
    1.16  fun mk_app _ p [] = p