diff -r 219924615db6 -r a6e25644b845 src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Tue Dec 05 18:33:29 2006 +0100
+++ b/src/Pure/General/xml.ML	Tue Dec 05 19:33:15 2006 +0100
@@ -19,7 +19,8 @@
       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   *)
-  type element = string * attributes * tree list
+  type content = tree list
+  type element = string * attributes * content
   val string_of_tree: tree -> string
   val buffer_of_tree: tree -> Buffer.T
   val parse_string : string -> string option
@@ -86,7 +87,9 @@
   | Text of string      
   | Rawtext of string;  
 
-type element = string * attributes * tree list
+type content = tree list
+
+type element = string * attributes * content
 
 fun buffer_of_tree tree =
   let