src/Pure/General/bytes.ML
changeset 80803 7e39c785ca5d
parent 80794 d4c489401844
child 80877 e55723709fab
--- a/src/Pure/General/bytes.ML	Mon Sep 02 20:12:52 2024 +0200
+++ b/src/Pure/General/bytes.ML	Mon Sep 02 20:54:00 2024 +0200
@@ -211,13 +211,4 @@
 
 fun write path bytes = File_Stream.open_output (fn stream => write_stream stream bytes) path;
 
-
-(* ML pretty printing *)
-
-val _ =
-  ML_system_pp (fn _ => fn _ => fn bytes =>
-    PolyML.PrettyString
-     (if is_empty bytes then "Bytes.empty"
-      else "Bytes {size = " ^ string_of_int (size bytes) ^ "}"))
-
 end;