# HG changeset patch
# User wenzelm
# Date 1712342514 -7200
# Node ID bda75c790bfa82dd16af3631d6f0859fe247e649
# Parent  1b986e5f9764a7bef014fdf833e2934cbdb16ef2
proper Scala code for String.literal_of_asciis: avoid ambiguity of ("" ++ ...);

diff -r 1b986e5f9764 -r bda75c790bfa src/HOL/String.thy
--- a/src/HOL/String.thy	Fri Apr 05 17:47:09 2024 +0200
+++ b/src/HOL/String.thy	Fri Apr 05 20:41:54 2024 +0200
@@ -803,7 +803,7 @@
     (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\"))"
+    and (Scala) "_.map((k: BigInt) => if (BigInt(0) <= k && k < BigInt(128)) k.charValue else 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"