diff -r 64dc09f7f189 -r 9de19e3a7231 src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Wed Sep 11 20:45:17 2024 +0200
+++ b/src/Pure/PIDE/yxml.ML	Wed Sep 11 21:25:15 2024 +0200
@@ -27,7 +27,6 @@
   val write_body: Path.T -> XML.body -> unit
   val output_markup_only: Markup.T -> string
   val output_markup_elem: Markup.T -> (string * string) * string
-  val markup_ops: Markup.ops
   val parse_body: string -> XML.body
   val parse_body_bytes: Bytes.T -> XML.body
   val parse: string -> XML.tree
@@ -85,8 +84,6 @@
   let val [bg1, bg2, en] = space_explode Z (string_of (XML.wrap_elem ((markup, Z_text), Z_text)))
   in ((bg1, bg2), en) end;
 
-val markup_ops: Markup.ops = {output = output_markup};
-
 
 
 (** efficient YXML parsing **)