src/Pure/Thy/html.scala

--- a/src/Pure/Thy/html.scala	Mon Mar 29 22:43:56 2010 +0200
+++ b/src/Pure/Thy/html.scala	Mon Mar 29 22:55:57 2010 +0200
@@ -41,13 +41,13 @@
         val t = new StringBuilder
         def flush() {
           if (!t.isEmpty) {
-            ts + XML.Text(t.toString)
+            ts += XML.Text(t.toString)
             t.clear
           }
         }
         def add(elem: XML.Tree) {
           flush()
-          ts + elem
+          ts += elem
         }
         val syms = Symbol.iterator(txt).map(_.toString)
         while (syms.hasNext) {