# HG changeset patch
# User haftmann
# Date 1737959989 -3600
# Node ID e23bd621eddb03cb6827ffa8d44e56385dafb9da
# Parent  6c052e21664f277ab43f2d5e48c0592f3ae2c88b
more correct SML for SML/NJ

diff -r 6c052e21664f -r e23bd621eddb src/HOL/Library/Code_Target_Bit_Shifts.thy
--- a/src/HOL/Library/Code_Target_Bit_Shifts.thy	Mon Jan 27 07:39:48 2025 +0100
+++ b/src/HOL/Library/Code_Target_Bit_Shifts.thy	Mon Jan 27 07:39:49 2025 +0100
@@ -51,7 +51,11 @@
 fun fold _ [] y = y
   | fold f (x :: xs) y = fold f xs (f x y);
 
-fun replicate n x = (if n <= 0 then [] else x :: replicate (n - 1) x);
+fun positive n = IntInf.> (n, 0);
+
+fun decr n = IntInf.- (n, 1);
+
+fun replicate n x = (if positive n then x :: replicate (decr n) x else []);
 
 val exp = curry IntInf.pow 2;