# HG changeset patch
# User wenzelm
# Date 1331238954 -3600
# Node ID c54b81bb9588e7a6056c8a46f2adb5eefafe5023
# Parent  5bdd68f380b37b1ba831c856b24c8ea0eb7e10a5
tuned;

diff -r 5bdd68f380b3 -r c54b81bb9588 src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Mar 08 19:56:57 2012 +0100
+++ b/src/Pure/library.ML	Thu Mar 08 21:35:54 2012 +0100
@@ -470,9 +470,9 @@
   let
     fun get (_: int) [] = NONE
       | get i (x :: xs) =
-          case f x
-           of NONE => get (i + 1) xs
-            | SOME y => SOME (i, y)
+          (case f x of
+            NONE => get (i + 1) xs
+          | SOME y => SOME (i, y))
   in get 0 end;
 
 val flat = List.concat;