--- 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")