diff -r d4bff63bcbf1 -r 0a83608e21f1 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Tue Jul 14 16:27:34 2009 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Wed Jul 15 10:11:13 2009 +0200
@@ -320,9 +320,7 @@
   returns @{text "0"}.
 *}
 
-definition
-  int :: "nat \<Rightarrow> int"
-where
+definition int :: "nat \<Rightarrow> int" where
   [code del]: "int = of_nat"
 
 lemma int_code' [code]:
@@ -336,6 +334,10 @@
 lemma of_nat_int [code_unfold_post]:
   "of_nat = int" by (simp add: int_def)
 
+lemma of_nat_aux_int [code_unfold]:
+  "of_nat_aux (\<lambda>i. i + 1) k 0 = int k"
+  by (simp add: int_def Nat.of_nat_code)
+
 code_const int
   (SML "_")
   (OCaml "_")