1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Thu Jan 14 17:47:39 2010 +0100
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Thu Jan 14 17:54:54 2010 +0100
     1.3 @@ -309,6 +309,7 @@
     1.4    def equals(that: Nat): Boolean = this.value == that.value
     1.5  
     1.6    def as_BigInt: BigInt = this.value
     1.7 +  def as_Int: Int = this.value
     1.8  
     1.9    def +(that: Nat): Nat = new Nat(this.value + that.value)
    1.10    def -(that: Nat): Nat = Nat(this.value + that.value)
    1.11 @@ -407,7 +408,7 @@
    1.12    (SML "IntInf.toInt")
    1.13    (OCaml "_")
    1.14    (Haskell "fromEnum")
    1.15 -  (Scala "!_.as'_BigInt")
    1.16 +  (Scala "!_.as'_Int")
    1.17  
    1.18  code_const Code_Numeral.nat_of
    1.19    (SML "IntInf.fromInt")