src/Pure/General/yxml.ML

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