src/Pure/term.ML
changeset 40844 5895c525739d
parent 40841 82baff065334
child 42083 e1209fc7ecdc
     1.1 --- a/src/Pure/term.ML	Wed Dec 01 15:02:39 2010 +0100
     1.2 +++ b/src/Pure/term.ML	Wed Dec 01 15:03:44 2010 +0100
     1.3 @@ -712,7 +712,7 @@
     1.4              val (vs, t') = expand_eta Ts (t $ Free (v, T)) used';
     1.5            in ((v, T) :: vs, t') end;
     1.6      val ((vs1, t'), (k', used')) = strip_abs t (k, used);
     1.7 -    val Ts = (fst o chop k' o fst o strip_type o fastype_of) t';
     1.8 +    val Ts = fst (chop k' (binder_types (fastype_of t')));
     1.9      val (vs2, t'') = expand_eta Ts t' used';
    1.10    in (vs1 @ vs2, t'') end;
    1.11