src/HOL/Library/Efficient_Nat.thy

--- a/src/HOL/Library/Efficient_Nat.thy	Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Tue May 19 16:54:55 2009 +0200
@@ -369,12 +369,12 @@
 
 text {* Conversion from and to indices. *}
 
-code_const Code_Index.of_nat
+code_const Code_Numeral.of_nat
   (SML "IntInf.toInt")
   (OCaml "Big'_int.int'_of'_big'_int")
   (Haskell "fromEnum")
 
-code_const Code_Index.nat_of
+code_const Code_Numeral.nat_of
   (SML "IntInf.fromInt")
   (OCaml "Big'_int.big'_int'_of'_int")
   (Haskell "toEnum")