diff -r 520148f9921d -r f968f4e3d520 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Mar 31 15:34:37 2014 +0200
+++ b/src/Pure/General/symbol.scala	Mon Mar 31 17:41:45 2014 +0200
@@ -166,7 +166,8 @@
     }
     def decode(symbol_range: Range): Text.Range = symbol_range.map(decode(_))
 
-    override def hashCode: Int = index.hashCode
+    private val hash: Int = index.toList.hashCode
+    override def hashCode: Int = hash
     override def equals(that: Any): Boolean =
       that match {
         case other: Index => index.sameElements(other.index)