removed obsolete XML.Output workaround;

--- a/src/Pure/General/xml.ML	Thu Aug 28 00:33:08 2008 +0200
+++ b/src/Pure/General/xml.ML	Thu Aug 28 00:33:09 2008 +0200
@@ -11,7 +11,6 @@
   datatype tree =
       Elem of string * attributes * tree list
     | Text of string
-    | Output of output
   val add_content: tree -> Buffer.T -> Buffer.T
   val detect: string -> bool
   val header: string
@@ -36,12 +35,10 @@
 
 datatype tree =
     Elem of string * attributes * tree list
-  | Text of string
-  | Output of output;   (* FIXME !? *)
+  | Text of string;
 
 fun add_content (Elem (_, _, ts)) = fold add_content ts
-  | add_content (Text s) = Buffer.add s
-  | add_content (Output _) = I;    (* FIXME !? *)
+  | add_content (Text s) = Buffer.add s;
 
 
 
@@ -96,8 +93,7 @@
           Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #>
           fold traverse ts #>
           Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
-      | traverse (Text s) = Buffer.add (text s)
-      | traverse (Output s) = Buffer.add s;
+      | traverse (Text s) = Buffer.add (text s);
   in Buffer.empty |> traverse tree end;
 
 val string_of = Buffer.content o buffer_of;

--- 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;