src/Pure/General/seq.ML

   val make: (unit -> ('a * 'a seq) option) -> 'a seq
   val pull: 'a seq -> ('a * 'a seq) option
   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
   val list_of: 'a seq -> 'a list
   val of_list: 'a list -> 'a seq

 
 (*head and tail -- beware of calling the sequence function twice!!*)
 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*)
 fun chop (n, xq) =
   if n <= 0 then ([], xq)