diff -r 92dfacb32053 -r c385c4eabb3b src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Fri Oct 12 08:20:46 2007 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Fri Oct 12 08:21:09 2007 +0200
@@ -6,7 +6,7 @@
 header {* Implementation of natural numbers by integers *}
 
 theory Efficient_Nat
-imports Main Pretty_Int
+imports Main Code_Integer
 begin
 
 text {*
@@ -165,13 +165,13 @@
   then show ?thesis unfolding int_aux_def int_of_nat_def by auto
 qed
 
-lemma ml_int_of_nat_code [code func, code inline]:
-  "ml_int_of_nat n = ml_int_of_int (int_of_nat n)"
-  unfolding ml_int_of_nat_def int_of_nat_def by simp
+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_mlt_int_code [code func, code inline]:
-  "nat_of_ml_int k = nat (int_of_ml_int k)"
-  unfolding nat_of_ml_int_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 *}