1.1 --- a/src/Pure/General/xml.ML	Fri Feb 16 22:46:03 2007 +0100
     1.2 +++ b/src/Pure/General/xml.ML	Sat Feb 17 17:18:47 2007 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4    datatype tree =
     1.5        Elem of string * attributes * tree list
     1.6      | Text of string    (* native string, subject to XML.text on output *)
     1.7 -    | Rawtext of string (* XML string: not parsed and output directly   *)
     1.8 +    | Rawtext of string (* XML string: output directly, not parsed      *)
     1.9    type content = tree list
    1.10    type element = string * attributes * content
    1.11    val string_of_tree: tree -> string