src/Pure/General/xml.ML

--- a/src/Pure/General/xml.ML	Tue Aug 10 20:13:52 2010 +0200
+++ b/src/Pure/General/xml.ML	Tue Aug 10 22:26:23 2010 +0200
@@ -10,6 +10,7 @@
   datatype tree =
       Elem of Markup.T * tree list
     | Text of string
+  type body = tree list
   val add_content: tree -> Buffer.T -> Buffer.T
   val header: string
   val text: string -> string
@@ -35,6 +36,8 @@
     Elem of Markup.T * tree list
   | Text of string;
 
+type body = tree list;
+
 fun add_content (Elem (_, ts)) = fold add_content ts
   | add_content (Text s) = Buffer.add s;