# HG changeset patch
# User wenzelm
# Date 1720972614 -7200
# Node ID b2c14b489e600e298fc6f5aaecd16c99f485d437
# Parent  446b887e23c7f6b36320062b1a5673c5bd8ad546
tuned output, following Isabelle/Scala;

diff -r 446b887e23c7 -r b2c14b489e60 src/Pure/General/bytes.ML
--- a/src/Pure/General/bytes.ML	Sun Jul 14 17:49:30 2024 +0200
+++ b/src/Pure/General/bytes.ML	Sun Jul 14 17:56:54 2024 +0200
@@ -216,6 +216,8 @@
 
 val _ =
   ML_system_pp (fn _ => fn _ => fn bytes =>
-    PolyML.PrettyString ("Bytes {size = " ^ string_of_int (size bytes) ^ "}"))
+    PolyML.PrettyString
+     (if is_empty bytes then "Bytes.empty"
+      else "Bytes {size = " ^ string_of_int (size bytes) ^ "}"))
 
 end;