--- a/src/HOL/Import/lazy_seq.ML Wed Feb 15 21:35:13 2006 +0100
+++ b/src/HOL/Import/lazy_seq.ML Wed Feb 15 23:57:06 2006 +0100
@@ -21,6 +21,7 @@
val getItem : 'a seq -> ('a * 'a seq) option
val nth : 'a seq * int -> 'a
val take : 'a seq * int -> 'a seq
+ val take_at_most : 'a seq * int -> 'a list
val drop : 'a seq * int -> 'a seq
val rev : 'a seq -> 'a seq
val concat : 'a seq seq -> 'a seq
@@ -90,7 +91,7 @@
fun getItem (Seq s) = force s
fun make f = Seq (delay f)
-fun null s = isSome (getItem s)
+fun null s = is_none (getItem s)
local
fun F n NONE = n
@@ -148,6 +149,12 @@
else F' s n
end
+fun take_at_most (s,n) =
+ if n <= 0 then [] else
+ case getItem s of
+ NONE => []
+ | SOME (x,s') => x::(take_at_most (s',n-1))
+
local
fun F s 0 = s
| F NONE _ = raise Subscript