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