src/Pure/type_infer.ML
changeset 19012 2577ac76cdc6
parent 18996 1b11052ad601
child 19046 bc5c6c9b114e
     1.1 --- a/src/Pure/type_infer.ML	Sat Feb 11 17:17:45 2006 +0100
     1.2 +++ b/src/Pure/type_infer.ML	Sat Feb 11 17:17:47 2006 +0100
     1.3 @@ -342,7 +342,7 @@
     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 (Ts',Ts'') = Library.splitAt(length Ts, Ts_bTs');
     1.8 +        val (Ts', Ts'') = chop (length Ts) Ts_bTs';
     1.9          val xs = map Free (map fst bs ~~ Ts'');
    1.10          val ts'' = map (fn t => subst_bounds (xs, t)) ts';
    1.11        in (ts'', Ts') end;