src/Pure/term.ML

--- a/src/Pure/term.ML	Wed Dec 01 15:02:39 2010 +0100
+++ b/src/Pure/term.ML	Wed Dec 01 15:03:44 2010 +0100
@@ -712,7 +712,7 @@
             val (vs, t') = expand_eta Ts (t $ Free (v, T)) used';
           in ((v, T) :: vs, t') end;
     val ((vs1, t'), (k', used')) = strip_abs t (k, used);
-    val Ts = (fst o chop k' o fst o strip_type o fastype_of) t';
+    val Ts = fst (chop k' (binder_types (fastype_of t')));
     val (vs2, t'') = expand_eta Ts t' used';
   in (vs1 @ vs2, t'') end;