src/HOL/Library/Efficient_Nat.thy

   "nat_of_int (int' n) = n"
   using nat_of_int_def int'_def by simp
 
 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:
 *}

 
 text {*
   @{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")
   (Haskell "Integer")