src/Pure/General/pretty.scala

--- a/src/Pure/General/pretty.scala	Tue Sep 18 13:36:28 2012 +0200
+++ b/src/Pure/General/pretty.scala	Tue Sep 18 14:51:12 2012 +0200
@@ -146,7 +146,7 @@
 
   def string_of(input: XML.Body, margin: Int = margin_default,
       metric: String => Double = metric_default): String =
-    XML.content(formatted(input, margin, metric)).mkString
+    XML.content(formatted(input, margin, metric))
 
 
   /* unformatted output */
@@ -164,5 +164,5 @@
     input.flatMap(standard_format).flatMap(fmt)
   }
 
-  def str_of(input: XML.Body): String = XML.content(unformatted(input)).mkString
+  def str_of(input: XML.Body): String = XML.content(unformatted(input))
 }