diff -r d7786f56f081 -r 873c31d9f10d src/HOL/String.thy
--- a/src/HOL/String.thy	Tue Jan 12 13:36:01 2010 +0100
+++ b/src/HOL/String.thy	Wed Jan 13 08:56:15 2010 +0100
@@ -170,14 +170,16 @@
 
 code_reserved SML string
 code_reserved OCaml string
+code_reserved Scala string
 
 code_type literal
   (SML "string")
   (OCaml "string")
   (Haskell "String")
+  (Scala "String")
 
 setup {*
-  fold String_Code.add_literal_string ["SML", "OCaml", "Haskell"]
+  fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
 *}
 
 code_instance literal :: eq
@@ -187,7 +189,7 @@
   (SML "!((_ : string) = _)")
   (OCaml "!((_ : string) = _)")
   (Haskell infixl 4 "==")
-
+  (Scala infixl 5 "==")
 
 types_code
   "char" ("string")