diff -r 64559e1ca05b -r 1f9f973eed2a src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Tue Apr 24 14:17:57 2018 +0000
+++ b/src/Tools/Code/code_scala.ML	Tue Apr 24 14:17:58 2018 +0000
@@ -23,6 +23,24 @@
 
 val target = "Scala";
 
+val print_scala_string =
+  let
+    fun chr i = "\\u" ^ align_right "0" 4 (Int.fmt StringCvt.HEX i)
+    fun char c = if c = "'" then "\\'"
+      else if c = "\"" then "\\\""
+      else if c = "\\" then "\\\\"
+      else
+        let
+          val i = ord c
+        in
+          if i < 32 orelse i > 126
+          then chr i
+          else if i >= 128
+          then error "non-ASCII byte in Haskell string literal"
+          else c
+        end
+  in quote o translate_string char end;
+
 datatype scala_stmt = Fun of typscheme * ((iterm list * iterm) * (thm option * bool)) list
   | Datatype of vname list * ((string * vname list) * itype list) list
   | Class of (vname * ((class * class) list * (string * itype) list))
@@ -189,7 +207,7 @@
             val vars = intro_vars params reserved;
           in
             concat [print_defhead tyvars vars const vs params tys ty',
-              str ("sys.error(\"" ^ const ^ "\")")]
+              str ("sys.error(" ^ print_scala_string const ^ ")")]
           end
       | print_def const (vs, ty) eqs =
           let
@@ -432,19 +450,12 @@
     >> (fn case_insensitive => serialize_scala case_insensitive));
 
 val literals = let
-  fun char_scala c = if c = "'" then "\\'"
-    else if c = "\"" then "\\\""
-    else if c = "\\" then "\\\\"
-    else let val k = ord c
-    in if k < 32 orelse k > 126
-    then "\\u" ^ align_right "0" 4 (Int.fmt StringCvt.HEX k) else c end
   fun numeral_scala k =
     if ~2147483647 < k andalso k <= 2147483647
     then signed_string_of_int k
     else quote (signed_string_of_int k)
 in Literals {
-  literal_char = Library.enclose "'" "'" o char_scala,
-  literal_string = quote o translate_string char_scala,
+  literal_string = print_scala_string,
   literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
   literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
   infix_cons = (6, "::")