src/HOL/Library/Efficient_Nat.thy

--- a/src/HOL/Library/Efficient_Nat.thy	Fri Feb 06 09:05:19 2009 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Fri Feb 06 09:05:19 2009 +0100
@@ -376,12 +376,12 @@
 
 text {* Conversion from and to indices. *}
 
-code_const index_of_nat
+code_const Code_Index.of_nat
   (SML "IntInf.toInt")
   (OCaml "Big'_int.int'_of'_big'_int")
   (Haskell "fromEnum")
 
-code_const nat_of_index
+code_const Code_Index.nat_of
   (SML "IntInf.fromInt")
   (OCaml "Big'_int.big'_int'_of'_int")
   (Haskell "toEnum")