unused;

--- a/src/Pure/PIDE/xml.ML	Mon Apr 12 22:17:48 2021 +0200
+++ b/src/Pure/PIDE/xml.ML	Mon Apr 12 22:18:37 2021 +0200
@@ -35,7 +35,6 @@
     | Text of string
   type body = tree list
   val blob: string list -> body
-  val chunk: body -> tree
   val is_empty: tree -> bool
   val is_empty_body: body -> bool
   val xml_elemN: string
@@ -80,8 +79,6 @@
 
 val blob = map Text;
 
-fun chunk body = Elem (Markup.empty, body);
-
 fun is_empty (Text "") = true
   | is_empty _ = false;