diff -r e5e34bd28257 -r f9f7c34b7dd4 src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Sat Nov 02 10:56:53 2019 +0100
+++ b/src/Pure/PIDE/xml.ML	Sat Nov 02 12:02:27 2019 +0100
@@ -34,6 +34,7 @@
       Elem of (string * attributes) * tree list
     | Text of string
   type body = tree list
+  val blob: string list -> body
   val xml_elemN: string
   val xml_nameN: string
   val xml_bodyN: string
@@ -73,13 +74,9 @@
 
 (** XML trees **)
 
-type attributes = (string * string) list;
+open Output_Primitives.XML;
 
-datatype tree =
-    Elem of (string * attributes) * tree list
-  | Text of string;
-
-type body = tree list;
+val blob = map Text;
 
 
 (* wrapped elements *)