src/Pure/PIDE/yxml.ML
changeset 80820 db114ec720cb
parent 80563 36da6a3c79d6
child 80821 eb383d50564b
--- a/src/Pure/PIDE/yxml.ML	Fri Sep 06 19:17:29 2024 +0200
+++ b/src/Pure/PIDE/yxml.ML	Fri Sep 06 20:31:20 2024 +0200
@@ -33,7 +33,6 @@
   val parse_body_bytes: Bytes.T -> XML.body
   val parse: string -> XML.tree
   val parse_bytes: Bytes.T -> XML.tree
-  val content_of: string -> string
   val is_wellformed: string -> bool
 end;
 
@@ -170,8 +169,6 @@
 
 end;
 
-val content_of = parse_body #> XML.content_of;
-
 fun is_wellformed s = string_of_body (parse_body s) = s
   handle Fail _ => false;