src/Pure/General/symbol.ML

--- a/src/Pure/General/symbol.ML	Sun Sep 01 22:59:11 2024 +0200
+++ b/src/Pure/General/symbol.ML	Mon Sep 02 13:41:40 2024 +0200
@@ -114,7 +114,7 @@
 in
   fun spaces n =
     if n < 64 then Vector.nth spaces0 n
-    else replicate_string (n div 64) (Vector.nth spaces0 64) ^ Vector.nth spaces0 (n mod 64);
+    else implode (Vector.nth spaces0 (n mod 64) :: replicate (n div 64) (Vector.nth spaces0 64));
 end;
 
 val comment = "\<comment>";