src/Pure/type_infer.ML
changeset 13629 a46362d2b19b
parent 8611 49166d549426
child 13667 0009325e9af0
     1.1 --- a/src/Pure/type_infer.ML	Fri Oct 04 15:57:32 2002 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Mon Oct 07 19:01:51 2002 +0200
     1.3 @@ -331,9 +331,8 @@
     1.4      fun prep_output bs ts Ts =
     1.5        let
     1.6          val (Ts_bTs', ts') = typs_terms_of [] PTFree "??" (Ts @ map snd bs, ts);
     1.7 -        val len = length Ts;
     1.8 -        val Ts' = take (len, Ts_bTs');
     1.9 -        val xs = map Free (map fst bs ~~ drop (len, Ts_bTs'));
    1.10 +        val (Ts',Ts'') = Library.splitAt(length Ts, Ts_bTs');
    1.11 +        val xs = map Free (map fst bs ~~ Ts'');
    1.12          val ts'' = map (fn t => subst_bounds (xs, t)) ts';
    1.13        in (ts'', Ts') end;
    1.14