src/Pure/library.ML
changeset 69237 76696742fd30
parent 68149 9a4a6adb95b5
child 69468 54a95e1199cb
     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