--- a/src/Pure/General/seq.ML Thu Oct 11 19:22:00 2001 +0200
+++ b/src/Pure/General/seq.ML Thu Oct 11 19:22:15 2001 +0200
@@ -17,6 +17,7 @@
val empty: 'a seq
val cons: 'a * 'a seq -> 'a seq
val single: 'a -> 'a seq
+ val try: ('a -> 'b) -> 'a -> 'b seq
val hd: 'a seq -> 'a
val tl: 'a seq -> 'a seq
val chop: int * 'a seq -> 'a list * 'a seq
@@ -73,6 +74,12 @@
fun hd xq = #1 (the (pull xq))
and tl xq = #2 (the (pull xq));
+(*partial function as procedure*)
+fun try f x =
+ (case Library.try f x of
+ Some y => single y
+ | None => empty);
+
(*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*)