diff -r 96b56c98f346 -r bed02fca80b5 src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Fri Nov 04 18:18:30 2016 +0100 +++ b/src/Tools/Code/code_scala.ML Sat Nov 05 14:35:40 2016 +0100 @@ -443,7 +443,7 @@ else if c = "\\" then "\\\\" else let val k = ord c in if k < 32 orelse k > 126 - then "\\u" ^ align_right "0" 4 (radixstring (8, "0", k)) else c end + 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