src/HOL/Library/Code_Target_Bit_Shifts.thy

--- a/src/HOL/Library/Code_Target_Bit_Shifts.thy	Fri Jan 10 18:35:46 2025 +0100
+++ b/src/HOL/Library/Code_Target_Bit_Shifts.thy	Fri Jan 10 21:08:18 2025 +0100
@@ -148,7 +148,10 @@
 private val maxIndex : BigInt = BigInt(Int.MaxValue);
 
 private def replicate[A](i : BigInt, x : A) : List[A] =
-  if (i <= 0) Nil else x :: replicate[A](i - 1, x)
+  i <= 0 match {
+    case true => Nil
+    case false => x :: replicate[A](i - 1, x)
+  }
 
 private def splitIndex(i : BigInt) : List[Int] = {
   val (b, s) = i /% maxIndex