diff -r 8c9925d31617 -r d7b5fb2e9ca2 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Tue Sep 18 11:49:23 2012 +0200
+++ b/src/Pure/General/pretty.scala	Tue Sep 18 13:18:45 2012 +0200
@@ -146,7 +146,7 @@
 
   def string_of(input: XML.Body, margin: Int = margin_default,
       metric: String => Double = metric_default): String =
-    formatted(input, margin, metric).iterator.flatMap(XML.content).mkString
+    XML.content(formatted(input, margin, metric)).mkString
 
 
   /* unformatted output */
@@ -164,6 +164,5 @@
     input.flatMap(standard_format).flatMap(fmt)
   }
 
-  def str_of(input: XML.Body): String =
-    unformatted(input).iterator.flatMap(XML.content).mkString
+  def str_of(input: XML.Body): String = XML.content(unformatted(input)).mkString
 }