author | haftmann |
Mon, 26 Jul 2010 11:10:36 +0200 | |
changeset 37969 | 3bf1fffcdd48 |
parent 37968 | 52fdcb76c0af |
child 37970 | f36980b37af5 |
--- a/src/HOL/Library/Efficient_Nat.thy Mon Jul 26 11:10:35 2010 +0200 +++ b/src/HOL/Library/Efficient_Nat.thy Mon Jul 26 11:10:36 2010 +0200 @@ -307,7 +307,7 @@ def as_BigInt: BigInt = this.value def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue) this.value.intValue - else this.value.intValue + else error("Int value out of range: " + this.value.toString) def +(that: Nat): Nat = new Nat(this.value + that.value) def -(that: Nat): Nat = Nat(this.value - that.value)