diff -r 885343964b7f -r b1ed84a5215b src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Wed Sep 11 12:18:29 2024 +0200
+++ b/src/Pure/PIDE/xml.ML	Wed Sep 11 12:32:11 2024 +0200
@@ -37,7 +37,6 @@
   val is_empty_body: body -> bool
   val string: string -> body
   val enclose: string -> string -> body -> body
-  val traverse_text: (string -> 'a -> 'a) -> XML.tree -> 'a -> 'a
   val trim_blanks: body -> body
   val filter_elements: {remove: string -> bool, expose: string -> bool} -> body -> body
   val header: string
@@ -93,17 +92,6 @@
 fun enclose bg en body = string bg @ body @ string en;
 
 
-(* traverse text *)
-
-fun traverse_text f tree =
-  (case unwrap_elem_body tree of
-    SOME ts => fold (traverse_text f) ts
-  | NONE =>
-      (case tree of
-        Elem (_, ts) => fold (traverse_text f) ts
-      | Text s => f s));
-
-
 (* trim blanks *)
 
 fun trim_blanks trees =