--- a/src/HOL/Imperative_HOL/Array.thy Sat Jan 16 22:52:43 2021 +0100
+++ b/src/HOL/Imperative_HOL/Array.thy Sun Jan 17 00:16:14 2021 +0100
@@ -486,7 +486,7 @@
text \<open>Scala\<close>
-code_printing type_constructor array \<rightharpoonup> (Scala) "!collection.mutable.ArraySeq[_]"
+code_printing type_constructor array \<rightharpoonup> (Scala) "!Array.T[_]"
code_printing constant Array \<rightharpoonup> (Scala) "!sys.error(\"bare Array\")"
code_printing constant Array.new' \<rightharpoonup> (Scala) "('_: Unit)/ => / Array.alloc((_))((_))"
code_printing constant Array.make' \<rightharpoonup> (Scala) "('_: Unit)/ =>/ Array.make((_))((_))"