# HG changeset patch
# User wenzelm
# Date 1725112896 -7200
# Node ID d4c489401844459ddcd4830c8bfab56e773b919e
# Parent  90f6e541e926da5c0021ebcc9583c23e8bb42ffa
avoid redundant XML.blob: Bytes.contents consist of larger chunks;

diff -r 90f6e541e926 -r d4c489401844 src/Pure/General/bytes.ML
--- a/src/Pure/General/bytes.ML	Sat Aug 31 16:00:16 2024 +0200
+++ b/src/Pure/General/bytes.ML	Sat Aug 31 16:01:36 2024 +0200
@@ -65,7 +65,7 @@
 fun contents (Bytes {buffer, chunks, ...}) =
   rev (chunks |> not (null buffer) ? cons (compact buffer));
 
-val contents_blob = contents #> XML.blob;
+val contents_blob = contents #> map XML.Text;
 
 val content = implode o contents;