--- a/src/Pure/General/seq.ML Tue Feb 10 17:53:51 2009 -0800
+++ b/src/Pure/General/seq.ML Wed Feb 11 14:48:14 2009 +1100
@@ -19,6 +19,7 @@
val hd: 'a seq -> 'a
val tl: 'a seq -> 'a seq
val chop: int -> 'a seq -> 'a list * 'a seq
+ val take: int -> 'a seq -> 'a seq
val list_of: 'a seq -> 'a list
val of_list: 'a list -> 'a seq
val append: 'a seq -> 'a seq -> 'a seq
@@ -94,6 +95,12 @@
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;
+
(*conversion from sequence to list*)
fun list_of xq =
(case pull xq of