1.1 --- a/src/HOL/Library/Efficient_Nat.thy Tue Jul 20 06:35:29 2010 +0200
1.2 +++ b/src/HOL/Library/Efficient_Nat.thy Tue Jul 20 08:54:21 2010 +0200
1.3 @@ -312,7 +312,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 = if (this.value >= Math.MIN_INT && this.value <= Math.MAX_INT)
1.8 + def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
1.9 this.value.intValue
1.10 else this.value.intValue
1.11