diff -r 52fdcb76c0af -r 3bf1fffcdd48 src/HOL/Library/Efficient_Nat.thy
--- 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)