--- a/src/Pure/library.ML Wed May 13 10:21:28 1998 +0200
+++ b/src/Pure/library.ML Wed May 13 12:17:30 1998 +0200
@@ -84,6 +84,7 @@
val find_index: ('a -> bool) -> 'a list -> int
val find_index_eq: ''a -> ''a list -> int
val find_first: ('a -> bool) -> 'a list -> 'a option
+ val get_first: ('a -> 'b option) -> 'a list -> 'b option
val flat: 'a list list -> 'a list
val seq: ('a -> unit) -> 'a list -> unit
val separate: 'a -> 'a list -> 'a list
@@ -471,6 +472,13 @@
| find_first pred (x :: xs) =
if pred x then Some x else find_first pred xs;
+(*get first element by lookup function*)
+fun get_first _ [] = None
+ | get_first f (x :: xs) =
+ (case f x of
+ None => get_first f xs
+ | some => some);
+
(*flatten a list of lists to a list*)
fun flat (ls: 'c list list) : 'c list = foldr (op @) (ls, []);