tuned;

--- 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>";

--- a/src/Pure/library.ML	Sun Sep 01 22:59:11 2024 +0200
+++ b/src/Pure/library.ML	Mon Sep 02 13:41:40 2024 +0200
@@ -505,13 +505,9 @@
   | surround s [] = [s];
 
 (*make the list [x, x, ..., x] of length n*)
-fun replicate (n: int) x =
-  let fun rep (0, xs) = xs
-        | rep (n, xs) = rep (n - 1, x :: xs)
-  in
-    if n < 0 then raise Subscript
-    else rep (n, [])
-  end;
+fun replicate n x =
+  if n < 0 then raise Subscript
+  else build (funpow n (cons x));
 
 
 (* direct product *)