diff -r ac9e909fe55d -r 0a2371e7ced3 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Fri Feb 15 08:31:30 2013 +0100
+++ b/src/Tools/Code/code_scala.ML	Fri Feb 15 08:31:31 2013 +0100
@@ -399,9 +399,6 @@
   literal_char = Library.enclose "'" "'" o char_scala,
   literal_string = quote o translate_string char_scala,
   literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
-  literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
-  literal_alternative_numeral = fn k => "Natural(" ^ numeral_scala k ^ ")",
-  literal_naive_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
   literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
   infix_cons = (6, "::")
 } end;