src/Pure/General/symbol.scala

--- a/src/Pure/General/symbol.scala	Fri Jul 08 22:00:53 2011 +0200
+++ b/src/Pure/General/symbol.scala	Sat Jul 09 12:56:51 2011 +0200
@@ -120,7 +120,7 @@
 
   class Index(text: CharSequence)
   {
-    case class Entry(chr: Int, sym: Int)
+    sealed case class Entry(chr: Int, sym: Int)
     val index: Array[Entry] =
     {
       val matcher = new Matcher(text)