--- a/src/HOL/Library/Efficient_Nat.thy Thu Jan 14 17:47:39 2010 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy Thu Jan 14 17:54:54 2010 +0100
@@ -309,6 +309,7 @@
def equals(that: Nat): Boolean = this.value == that.value
def as_BigInt: BigInt = this.value
+ def as_Int: Int = this.value
def +(that: Nat): Nat = new Nat(this.value + that.value)
def -(that: Nat): Nat = Nat(this.value + that.value)
@@ -407,7 +408,7 @@
(SML "IntInf.toInt")
(OCaml "_")
(Haskell "fromEnum")
- (Scala "!_.as'_BigInt")
+ (Scala "!_.as'_Int")
code_const Code_Numeral.nat_of
(SML "IntInf.fromInt")