diff -r 6960410f134d -r 852bce03412a src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Wed Jan 02 15:14:22 2008 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Wed Jan 02 15:14:23 2008 +0100
@@ -165,14 +165,6 @@
   then show ?thesis unfolding int_aux_def int_of_nat_def by auto
 qed
 
-lemma index_of_nat_code [code func, code inline]:
-  "index_of_nat n = index_of_int (int_of_nat n)"
-  unfolding index_of_nat_def int_of_nat_def by simp
-
-lemma nat_of_index_code [code func, code inline]:
-  "nat_of_index k = nat (int_of_index k)"
-  unfolding nat_of_index_def by simp
-
 
 subsection {* Code generator setup for basic functions *}
 
@@ -221,11 +213,22 @@
   (OCaml "_")
   (Haskell "_")
 
+code_const index_of_nat
+  (SML "_")
+  (OCaml "_")
+  (Haskell "_")
+
 code_const nat_of_int
   (SML "_")
   (OCaml "_")
   (Haskell "_")
 
+code_const nat_of_index
+  (SML "_")
+  (OCaml "_")
+  (Haskell "_")
+
+
 text {* Using target language div and mod *}
 
 code_const "op div \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"