tuned (see map_index);

--- a/src/Pure/library.ML	Mon Nov 05 11:29:11 2018 +0100
+++ b/src/Pure/library.ML	Mon Nov 05 15:00:22 2018 +0100
@@ -448,12 +448,12 @@
 
 fun get_index f =
   let
-    fun get (_: int) [] = NONE
-      | get i (x :: xs) =
+    fun get_aux (_: int) [] = NONE
+      | get_aux i (x :: xs) =
           (case f x of
-            NONE => get (i + 1) xs
+            NONE => get_aux (i + 1) xs
           | SOME y => SOME (i, y))
-  in get 0 end;
+  in get_aux 0 end;
 
 val flat = List.concat;