src/Pure/library.ML

--- a/src/Pure/library.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/Pure/library.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -126,6 +126,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_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
   val get_first: ('a -> 'b option) -> 'a list -> 'b option
   val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
@@ -632,6 +633,15 @@
         NONE => get_first f xs
       | some => some);
 
+fun get_index f =
+  let
+    fun get _ [] = NONE
+      | get i (x::xs) = 
+          case f x
+           of NONE => get (i+1) xs
+            | SOME y => SOME (i, y)
+  in get 0 end;
+
 (*flatten a list of lists to a list*)
 val flat = List.concat;