tuned (see map_index);
authorwenzelm
Mon Nov 05 15:00:22 2018 +0100 (6 months ago)
changeset 6923776696742fd30
parent 69236 a75aab6d785b
child 69238 d98cfb369cbd
tuned (see map_index);
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Mon Nov 05 11:29:11 2018 +0100
     1.2 +++ b/src/Pure/library.ML	Mon Nov 05 15:00:22 2018 +0100
     1.3 @@ -448,12 +448,12 @@
     1.4  
     1.5  fun get_index f =
     1.6    let
     1.7 -    fun get (_: int) [] = NONE
     1.8 -      | get i (x :: xs) =
     1.9 +    fun get_aux (_: int) [] = NONE
    1.10 +      | get_aux i (x :: xs) =
    1.11            (case f x of
    1.12 -            NONE => get (i + 1) xs
    1.13 +            NONE => get_aux (i + 1) xs
    1.14            | SOME y => SOME (i, y))
    1.15 -  in get 0 end;
    1.16 +  in get_aux 0 end;
    1.17  
    1.18  val flat = List.concat;
    1.19