diff -r bda75c790bfa -r 5afbf04418ec src/HOL/String.thy
--- a/src/HOL/String.thy	Fri Apr 05 20:41:54 2024 +0200
+++ b/src/HOL/String.thy	Fri Apr 05 21:21:02 2024 +0200
@@ -803,12 +803,12 @@
     (SML) "Str'_Literal.literal'_of'_asciis"
     and (OCaml) "Str'_Literal.literal'_of'_asciis"
     and (Haskell) "map/ (let chr k | (0 <= k && k < 128) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)"
-    and (Scala) "_.map((k: BigInt) => if (BigInt(0) <= k && k < BigInt(128)) k.charValue else sys.error(\"Non-ASCII character in literal\")).mkString"
+    and (Scala) "_.map((k: BigInt) => BigInt(0) <= k && k < BigInt(128) match { case true => k.charValue case false => sys.error(\"Non-ASCII character in literal\") }).mkString"
 | constant String.asciis_of_literal \<rightharpoonup>
     (SML) "Str'_Literal.asciis'_of'_literal"
     and (OCaml) "Str'_Literal.asciis'_of'_literal"
     and (Haskell) "map/ (let ord k | (k < 128) = Prelude.toInteger k in ord . (Prelude.fromEnum :: Prelude.Char -> Prelude.Int))"
-    and (Scala) "!(_.toList.map(c => { val k: Int = c.toInt; if (k < 128) BigInt(k) else sys.error(\"Non-ASCII character in literal\") }))"
+    and (Scala) "!(_.toList.map(c => { val k: Int = c.toInt; k < 128 match { case true => BigInt(k) case false => sys.error(\"Non-ASCII character in literal\") } }))"
 | class_instance String.literal :: equal \<rightharpoonup>
     (Haskell) -
 | constant "HOL.equal :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>