Scala "\u" notation uses hexadecimal, not octal (amending 00a135c0a17f);

--- 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