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 *)