src/HOL/Library/Efficient_Nat.thy

 *}
 
 code_reserved Haskell Nat
 
 code_include Scala "Nat" {*
+import scala.Math
+
 object Nat {
 
   def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
   def apply(numeral: Int): Nat = Nat(BigInt(numeral))
   def apply(numeral: String): Nat = Nat(BigInt(numeral))

   override def toString(): String = this.value.toString
 
   def equals(that: Nat): Boolean = this.value == that.value
 
   def as_BigInt: BigInt = this.value
-  def as_Int: Int = this.value
+  def as_Int: Int = if (this.value >= Math.MAX_INT && this.value <= Math.MAX_INT)
+      this.value.intValue
+    else error("Int value too big:" + this.value.toString)
 
   def +(that: Nat): Nat = new Nat(this.value + that.value)
   def -(that: Nat): Nat = Nat(this.value + that.value)
   def *(that: Nat): Nat = new Nat(this.value * that.value)
 

   -- {* this interacts as desired with @{thm nat_number_of_def} *}
   by (simp add: number_nat_inst.number_of_nat)
 
 setup {*
   fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat}
-    false true Code_Printer.str) ["SML", "OCaml", "Haskell"]
+    false Code_Printer.literal_positive_numeral) ["SML", "OCaml", "Haskell"]
   #> Numeral.add_code @{const_name number_nat_inst.number_of_nat}
-    false true (fn s => (Pretty.block o map Code_Printer.str) ["Nat.Nat", s]) "Scala"
+    false Code_Printer.literal_positive_numeral "Scala"
 *}
 
 text {*
   Since natural numbers are implemented
   using integers in ML, the coercion function @{const "of_nat"} of type