src/Pure/General/yxml.scala

--- a/src/Pure/General/yxml.scala	Tue Aug 10 22:26:23 2010 +0200
+++ b/src/Pure/General/yxml.scala	Tue Aug 10 23:03:48 2010 +0200
@@ -59,7 +59,7 @@
   }
 
 
-  def parse_body(source: CharSequence): List[XML.Tree] =
+  def parse_body(source: CharSequence): XML.Body =
   {
     /* stack operations */
 
@@ -120,7 +120,7 @@
     XML.elem (Markup.MALFORMED,
       List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
 
-  def parse_body_failsafe(source: CharSequence): List[XML.Tree] =
+  def parse_body_failsafe(source: CharSequence): XML.Body =
   {
     try { parse_body(source) }
     catch { case _: RuntimeException => List(markup_failsafe(source)) }