diff -r 5ba68d3bd741 -r 3bb6468d202e src/Pure/General/bytes.ML
--- a/src/Pure/General/bytes.ML	Fri Apr 14 20:42:17 2023 +0200
+++ b/src/Pure/General/bytes.ML	Fri Apr 14 21:34:51 2023 +0200
@@ -158,7 +158,7 @@
   else if size sep <> 1 then [content bytes]
   else
     let
-      val sep_char = String.sub (sep, 0);
+      val sep_char = String.nth sep 0;
 
       fun add_part s part =
         Buffer.add (Substring.string s) (the_default Buffer.empty part);