--- a/src/HOL/Library/EfficientNat.thy Fri Mar 23 09:40:49 2007 +0100
+++ b/src/HOL/Library/EfficientNat.thy Fri Mar 23 09:40:50 2007 +0100
@@ -148,6 +148,8 @@
@{typ nat} is no longer a datatype but embedded into the integers.
*}
+code_datatype nat_of_int
+
code_const "0::nat"
(SML "!(0 : IntInf.int)")
(OCaml "Big'_int.big'_int'_of'_int/ 0")
@@ -158,10 +160,6 @@
(OCaml "Big_int.succ'_big'_int")
(Haskell "!((_) + 1)")
-setup {*
- CodegenData.add_datatype ("nat", ([], []))
-*}
-
types_code
nat ("int")
attach (term_of) {*