src/Pure/General/position.scala

--- a/src/Pure/General/position.scala	Mon Aug 25 16:52:11 2008 +0200
+++ b/src/Pure/General/position.scala	Mon Aug 25 20:01:17 2008 +0200
@@ -22,7 +22,7 @@
       case None => None
       case Some(value) =>
         try { Some(Integer.parseInt(value)) }
-        catch { case e: NumberFormatException => None }
+        catch { case _: NumberFormatException => None }
     }
   }