1.1 --- a/src/Pure/General/xml.ML	Thu Aug 28 00:33:08 2008 +0200
     1.2 +++ b/src/Pure/General/xml.ML	Thu Aug 28 00:33:09 2008 +0200
     1.3 @@ -11,7 +11,6 @@
     1.4    datatype tree =
     1.5        Elem of string * attributes * tree list
     1.6      | Text of string
     1.7 -    | Output of output
     1.8    val add_content: tree -> Buffer.T -> Buffer.T
     1.9    val detect: string -> bool
    1.10    val header: string
    1.11 @@ -36,12 +35,10 @@
    1.12  
    1.13  datatype tree =
    1.14      Elem of string * attributes * tree list
    1.15 -  | Text of string
    1.16 -  | Output of output;   (* FIXME !? *)
    1.17 +  | Text of string;
    1.18  
    1.19  fun add_content (Elem (_, _, ts)) = fold add_content ts
    1.20 -  | add_content (Text s) = Buffer.add s
    1.21 -  | add_content (Output _) = I;    (* FIXME !? *)
    1.22 +  | add_content (Text s) = Buffer.add s;
    1.23  
    1.24  
    1.25  
    1.26 @@ -96,8 +93,7 @@
    1.27            Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #>
    1.28            fold traverse ts #>
    1.29            Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
    1.30 -      | traverse (Text s) = Buffer.add (text s)
    1.31 -      | traverse (Output s) = Buffer.add s;
    1.32 +      | traverse (Text s) = Buffer.add (text s);
    1.33    in Buffer.empty |> traverse tree end;
    1.34  
    1.35  val string_of = Buffer.content o buffer_of;

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