tuned;
authorwenzelm
Thu Mar 08 21:35:54 2012 +0100 (2012-03-08)
changeset 46838c54b81bb9588
parent 46837 5bdd68f380b3
child 46839 f7232c078fa5
tuned;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Thu Mar 08 19:56:57 2012 +0100
     1.2 +++ b/src/Pure/library.ML	Thu Mar 08 21:35:54 2012 +0100
     1.3 @@ -470,9 +470,9 @@
     1.4    let
     1.5      fun get (_: int) [] = NONE
     1.6        | get i (x :: xs) =
     1.7 -          case f x
     1.8 -           of NONE => get (i + 1) xs
     1.9 -            | SOME y => SOME (i, y)
    1.10 +          (case f x of
    1.11 +            NONE => get (i + 1) xs
    1.12 +          | SOME y => SOME (i, y))
    1.13    in get 0 end;
    1.14  
    1.15  val flat = List.concat;