# HG changeset patch
# User haftmann
# Date 1263488094 -3600
# Node ID 780172c006e15b53ca95b383284af052692f58ce
# Parent  0d6a2ae86525c4be76aba62d7d6b30b5478b5ae5
dedicated conversions to and from Int

diff -r 0d6a2ae86525 -r 780172c006e1 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Thu Jan 14 17:47:39 2010 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Thu Jan 14 17:54:54 2010 +0100
@@ -309,6 +309,7 @@
   def equals(that: Nat): Boolean = this.value == that.value
 
   def as_BigInt: BigInt = this.value
+  def as_Int: Int = this.value
 
   def +(that: Nat): Nat = new Nat(this.value + that.value)
   def -(that: Nat): Nat = Nat(this.value + that.value)
@@ -407,7 +408,7 @@
   (SML "IntInf.toInt")
   (OCaml "_")
   (Haskell "fromEnum")
-  (Scala "!_.as'_BigInt")
+  (Scala "!_.as'_Int")
 
 code_const Code_Numeral.nat_of
   (SML "IntInf.fromInt")