# HG changeset patch
# User haftmann
# Date 1234528094 -3600
# Node ID 9049a2bfbe6d1ff10aaeeebdc94ab6741ecb9901
# Parent  97ba7a7651dec11c0f57ecbf9d772590b340141a
made SMLNJ happy

diff -r 97ba7a7651de -r 9049a2bfbe6d src/Pure/General/seq.ML
--- a/src/Pure/General/seq.ML	Fri Feb 13 21:14:30 2009 +1100
+++ b/src/Pure/General/seq.ML	Fri Feb 13 13:28:14 2009 +0100
@@ -89,17 +89,17 @@
 (*the list of the first n elements, paired with rest of sequence;
   if length of list is less than n, then sequence had less than n elements*)
 fun chop n xq =
-  if n <= (0: int) then ([], xq)
+  if n <= (0 : int) then ([], xq)
   else
     (case pull xq of
       NONE => ([], xq)
     | SOME (x, xq') => apfst (Basics.cons x) (chop (n - 1) xq'));
 
-(* truncate the sequence after n elements *)
-fun take n s = let
-    fun f 0 _  () = NONE
-      | f n ss () = Option.map (apsnd (make o f (n - 1))) (pull ss);
-  in make (f n s) end;
+(*truncate the sequence after n elements*)
+fun take n xq =
+  if n <= (0 : int) then empty
+  else make (fn () =>
+    (Option.map o apsnd) (take (n - 1)) (pull xq));
 
 (*conversion from sequence to list*)
 fun list_of xq =