diff -r c0b5ff9e9e4d -r ae9cd0e92423 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Fri Aug 24 14:14:18 2007 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Fri Aug 24 14:14:20 2007 +0200
@@ -63,6 +63,8 @@
 lemma eq_nat_of_int: "int' n = x \<Longrightarrow> n = nat_of_int x"
 by (erule subst, simp only: nat_of_int_int)
 
+code_datatype nat_of_int
+
 text {*
   Case analysis on natural numbers is rephrased using a conditional
   expression:
@@ -161,8 +163,6 @@
   @{typ nat} is no longer a datatype but embedded into the integers.
 *}
 
-code_datatype nat_of_int
-
 code_type nat
   (SML "IntInf.int")
   (OCaml "Big'_int.big'_int")