1.1 --- a/src/Pure/General/yxml.ML	Thu Aug 28 00:33:08 2008 +0200
     1.2 +++ b/src/Pure/General/yxml.ML	Thu Aug 28 00:33:09 2008 +0200
     1.3 @@ -58,8 +58,7 @@
     1.4            Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #>
     1.5            fold tree ts #>
     1.6            Buffer.add XYX
     1.7 -      | tree (XML.Text s) = Buffer.add s
     1.8 -      | tree (XML.Output s) = Buffer.add s;
     1.9 +      | tree (XML.Text s) = Buffer.add s;
    1.10    in Buffer.empty |> tree t |> Buffer.content end;
    1.11  
    1.12