diff -r a5e7574d8214 -r 3ff725ac13a4 src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Mon Mar 29 01:07:01 2010 -0700
+++ b/src/Pure/General/xml.scala	Mon Mar 29 22:43:56 2010 +0200
@@ -36,7 +36,7 @@
   private def append_text(text: String, s: StringBuilder) {
     if (text == null) s ++ text
     else {
-      for (c <- text.elements) c match {
+      for (c <- text.iterator) c match {
         case '<' => s ++ "&lt;"
         case '>' => s ++ "&gt;"
         case '&' => s ++ "&amp;"