diff -r 4a76497f2eaa -r 7a3610dca96b src/HOL/Library/Code_Char.thy --- a/src/HOL/Library/Code_Char.thy Fri Jun 18 15:03:20 2010 +0200 +++ b/src/HOL/Library/Code_Char.thy Fri Jun 18 15:03:20 2010 +0200 @@ -58,12 +58,12 @@ (SML "String.implode") (OCaml "failwith/ \"implode\"") (Haskell "_") - (Scala "List.toString((_))") + (Scala "!(\"\" ++/ _)") code_const explode (SML "String.explode") (OCaml "failwith/ \"explode\"") (Haskell "_") - (Scala "List.fromString((_))") + (Scala "!(_.toList)") end