diff -r e97b22500a5c -r 970e1466028d src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Fri Jan 22 13:38:28 2010 +0100
+++ b/src/Tools/Code/code_scala.ML	Fri Jan 22 13:38:28 2010 +0100
@@ -404,17 +404,18 @@
     let
       val s = ML_Syntax.print_char c;
     in if s = "'" then "\\'" else s end;
-  fun bigint_scala k = "(" ^ (if k <= 2147483647
-    then string_of_int k else quote (string_of_int k)) ^ ")"
+  fun numeral_scala k = if k < 0
+    then if k <= 2147483647 then "- " ^ string_of_int (~ k)
+      else quote ("- " ^ string_of_int (~ k))
+    else if k <= 2147483647 then string_of_int k
+      else quote (string_of_int k)
 in Literals {
   literal_char = Library.enclose "'" "'" o char_scala,
   literal_string = quote o translate_string char_scala,
-  literal_numeral = fn unbounded => fn k => if k >= 0 then
-      if unbounded then bigint_scala k
-      else Library.enclose "(" ")" (string_of_int k)
-    else
-      if unbounded then "(- " ^ bigint_scala (~ k) ^ ")"
-      else Library.enclose "(" ")" (signed_string_of_int k),
+  literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
+  literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
+  literal_naive_numeral = fn k => if k >= 0
+    then string_of_int k else "(- " ^ string_of_int (~ k) ^ ")",
   literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
   infix_cons = (6, "::")
 } end;
@@ -442,7 +443,7 @@
       "true", "type", "val", "var", "while", "with"
     ]
   #> fold (Code_Target.add_reserved target) [
-      "error", "apply", "List", "Nil"
+      "error", "apply", "List", "Nil", "BigInt"
     ];
 
 end; (*struct*)