avoid Scala legacy operations
authorhaftmann
Fri Jun 18 15:03:20 2010 +0200 (2010-06-18)
changeset 374597a3610dca96b
parent 37458 4a76497f2eaa
child 37460 910b2422571d
avoid Scala legacy operations
src/HOL/Library/Code_Char.thy
     1.1 --- a/src/HOL/Library/Code_Char.thy	Fri Jun 18 15:03:20 2010 +0200
     1.2 +++ b/src/HOL/Library/Code_Char.thy	Fri Jun 18 15:03:20 2010 +0200
     1.3 @@ -58,12 +58,12 @@
     1.4    (SML "String.implode")
     1.5    (OCaml "failwith/ \"implode\"")
     1.6    (Haskell "_")
     1.7 -  (Scala "List.toString((_))")
     1.8 +  (Scala "!(\"\" ++/ _)")
     1.9  
    1.10  code_const explode
    1.11    (SML "String.explode")
    1.12    (OCaml "failwith/ \"explode\"")
    1.13    (Haskell "_")
    1.14 -  (Scala "List.fromString((_))")
    1.15 +  (Scala "!(_.toList)")
    1.16  
    1.17  end