diff -r a5e7574d8214 -r 3ff725ac13a4 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Mar 29 01:07:01 2010 -0700
+++ b/src/Pure/General/symbol.scala	Mon Mar 29 22:43:56 2010 +0200
@@ -7,7 +7,7 @@
 package isabelle
 
 import scala.io.Source
-import scala.collection.{jcl, mutable}
+import scala.collection.mutable
 import scala.util.matching.Regex
 
 
@@ -54,9 +54,9 @@
   }
 
 
-  /* elements */
+  /* iterator */
 
-  def elements(text: CharSequence) = new Iterator[CharSequence]
+  def iterator(text: CharSequence) = new Iterator[CharSequence]
   {
     private val matcher = new Matcher(text)
     private var i = 0
@@ -124,12 +124,7 @@
       }
       (min, max)
     }
-    private val table =
-    {
-      val table = new jcl.HashMap[String, String]   // reasonably efficient?
-      for ((x, y) <- list) table + (x -> y)
-      table
-    }
+    private val table = Map[String, String]() ++ list
     def recode(text: String): String =
     {
       val len = text.length