# HG changeset patch
# User haftmann
# Date 1279286903 -7200
# Node ID 6f8b1bb4d248b48aa7a2bd8ca785572d2933e228
# Parent  b70d7a3479642e3a01143468b6907538ee5a0f0a
corrected range chec

diff -r b70d7a347964 -r 6f8b1bb4d248 src/HOL/Library/Efficient_Nat.thy
--- 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)