src/Pure/type_infer.ML

--- a/src/Pure/type_infer.ML	Fri Oct 04 15:57:32 2002 +0200
+++ b/src/Pure/type_infer.ML	Mon Oct 07 19:01:51 2002 +0200
@@ -331,9 +331,8 @@
     fun prep_output bs ts Ts =
       let
         val (Ts_bTs', ts') = typs_terms_of [] PTFree "??" (Ts @ map snd bs, ts);
-        val len = length Ts;
-        val Ts' = take (len, Ts_bTs');
-        val xs = map Free (map fst bs ~~ drop (len, Ts_bTs'));
+        val (Ts',Ts'') = Library.splitAt(length Ts, Ts_bTs');
+        val xs = map Free (map fst bs ~~ Ts'');
         val ts'' = map (fn t => subst_bounds (xs, t)) ts';
       in (ts'', Ts') end;