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