diff -r 750b63fa4c4e -r 27925b58d6bd src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Tue Jul 02 20:47:32 2013 +0200
+++ b/src/Pure/General/symbol.scala	Wed Jul 03 15:11:15 2013 +0200
@@ -111,7 +111,12 @@
 
   /* decoding offsets */
 
-  class Index(text: CharSequence)
+  object Index
+  {
+    def apply(text: CharSequence): Index = new Index(text)
+  }
+
+  final class Index private(text: CharSequence)
   {
     sealed case class Entry(chr: Int, sym: Int)
     val index: Array[Entry] =