# HG changeset patch
# User haftmann
# Date 1279608861 -7200
# Node ID 3d8857f42a643437f829b9b870ce531c48e23d60
# Parent  c26f9d06e82c6d26c9a6658085a31ccdc0cd4e91
avoid deprecation

diff -r c26f9d06e82c -r 3d8857f42a64 src/HOL/Library/Efficient_Nat.thy
--- 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