# HG changeset patch
# User wenzelm
# Date 1002820935 -7200
# Node ID 0d60622b668f86eda1926b238be879476c3896ef
# Parent  5341e38309e8b270bbe7d7614cd1608aa5499c1c
added try;

diff -r 5341e38309e8 -r 0d60622b668f src/Pure/General/seq.ML
--- 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*)