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;