# HG changeset patch
# User wenzelm
# Date 895054650 -7200
# Node ID fe8b0c82691be9ea6be6f75df93ecfc7cc9c577f
# Parent  5ff99bd60da9462e1fb861fd19cd077acc83e977
get_first: ('a -> 'b option) -> 'a list -> 'b option;

diff -r 5ff99bd60da9 -r fe8b0c82691b src/Pure/library.ML
--- 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, []);