# HG changeset patch
# User haftmann
# Date 1736539698 -3600
# Node ID 8d790d757bfbb554349ff5c1206db5c4f5f95826
# Parent  a1dc03194053aef16b3a687a24b4bec7ba5dc2bf
compatibility with Scala 3

diff -r a1dc03194053 -r 8d790d757bfb 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