diff -r 6b3739fee456 -r 8953d4cc060a src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Mar 31 12:35:39 2014 +0200
+++ b/src/Pure/General/symbol.scala	Mon Mar 31 15:05:24 2014 +0200
@@ -165,6 +165,13 @@
       else index(i).chr + sym - index(i).sym
     }
     def decode(symbol_range: Range): Text.Range = symbol_range.map(decode(_))
+
+    override def hashCode: Int = index.hashCode
+    override def equals(that: Any): Boolean =
+      that match {
+        case other: Index => index.sameElements(other.index)
+        case _ => false
+      }
   }