1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Mon Jul 26 11:10:35 2010 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Mon Jul 26 11:10:36 2010 +0200
     1.3 @@ -307,7 +307,7 @@
     1.4    def as_BigInt: BigInt = this.value
     1.5    def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
     1.6        this.value.intValue
     1.7 -    else this.value.intValue
     1.8 +    else error("Int value out of range: " + this.value.toString)
     1.9  
    1.10    def +(that: Nat): Nat = new Nat(this.value + that.value)
    1.11    def -(that: Nat): Nat = Nat(this.value - that.value)