# HG changeset patch
# User wenzelm
# Date 1725277300 -7200
# Node ID 5d09ceca092475c5873e424b15b185c9ed5ea17c
# Parent  12efa7f92f35a53f80c4875317d30a713886ab9d
tuned;

diff -r 12efa7f92f35 -r 5d09ceca0924 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>";
diff -r 12efa7f92f35 -r 5d09ceca0924 src/Pure/library.ML
--- 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 *)