--- a/src/HOL/Library/Efficient_Nat.thy Fri Jul 16 15:28:22 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Fri Jul 16 15:28:23 2010 +0200
@@ -312,9 +312,9 @@
def equals(that: Nat): Boolean = this.value == that.value
def as_BigInt: BigInt = this.value
- def as_Int: Int = if (this.value >= Math.MAX_INT && this.value <= Math.MAX_INT)
+ def as_Int: Int = if (this.value >= Math.MIN_INT && this.value <= Math.MAX_INT)
this.value.intValue
- else error("Int value too big:" + this.value.toString)
+ else this.value.intValue
def +(that: Nat): Nat = new Nat(this.value + that.value)
def -(that: Nat): Nat = Nat(this.value - that.value)