# HG changeset patch
# User aspinall
# Date 1171729127 -3600
# Node ID 4c96d3370186328aa67f3172d6d77e1cf650ed6d
# Parent  652f316ca26abd701df2e257185906c15d04b915
Clarify comment

diff -r 652f316ca26a -r 4c96d3370186 src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Fri Feb 16 22:46:03 2007 +0100
+++ b/src/Pure/General/xml.ML	Sat Feb 17 17:18:47 2007 +0100
@@ -18,7 +18,7 @@
   datatype tree =
       Elem of string * attributes * tree list
     | Text of string    (* native string, subject to XML.text on output *)
-    | Rawtext of string (* XML string: not parsed and output directly   *)
+    | Rawtext of string (* XML string: output directly, not parsed      *)
   type content = tree list
   type element = string * attributes * content
   val string_of_tree: tree -> string