diff -r 39035276927c -r 132f99cc0a43 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Tue Jun 21 12:53:55 2011 +0200
+++ b/src/Pure/Thy/html.scala	Tue Jun 21 13:29:44 2011 +0200
@@ -73,7 +73,7 @@
             flush()
             ts += elem
           }
-          val syms = Symbol.iterator(txt).map(_.toString)
+          val syms = Symbol.iterator_string(txt)
           while (syms.hasNext) {
             val s1 = syms.next
             def s2() = if (syms.hasNext) syms.next else ""