changeset 37892 | 3d8857f42a64 |
parent 37878 | d016aaead7a2 |
child 37947 | 844977c7abeb |
--- a/src/HOL/Library/Efficient_Nat.thy Tue Jul 20 06:35:29 2010 +0200 +++ b/src/HOL/Library/Efficient_Nat.thy Tue Jul 20 08:54:21 2010 +0200 @@ -312,7 +312,7 @@ def equals(that: Nat): Boolean = this.value == that.value def as_BigInt: BigInt = this.value - def as_Int: Int = if (this.value >= Math.MIN_INT && this.value <= Math.MAX_INT) + def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue) this.value.intValue else this.value.intValue