src/Pure/library.ML

   val split_last: 'a list -> 'a list * 'a
   val nth_update: 'a -> int * 'a list -> 'a list
   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
   val replicate: int -> 'a -> 'a list
   val multiply: 'a list * 'a list list -> 'a list list

 (*find first element satisfying predicate*)
 fun find_first _ [] = None
   | 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, []);
 
 (*like Lisp's MAPC -- seq proc [x1, ..., xn] evaluates
   (proc x1; ...; proc xn) for side effects*)