src/Pure/System/message_channel.ML
changeset 73557 225486d9c960
parent 73262 71b7a5775342
child 73558 a5d1d1e2f109
--- a/src/Pure/System/message_channel.ML	Sat Apr 10 21:50:59 2021 +0200
+++ b/src/Pure/System/message_channel.ML	Sun Apr 11 21:23:51 2021 +0200
@@ -21,9 +21,7 @@
 
 datatype message = Message of {body: XML.body, flush: bool};
 
-fun body_size body = fold (YXML.traverse (Integer.add o size)) body 0;
-
-fun chunk body = XML.Text (string_of_int (body_size body) ^ "\n") :: body;
+fun chunk body = XML.Text (string_of_int (YXML.body_size body) ^ "\n") :: body;
 
 fun message name raw_props body =
   let