1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Fri Feb 06 09:05:19 2009 +0100
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Fri Feb 06 09:05:19 2009 +0100
     1.3 @@ -376,12 +376,12 @@
     1.4  
     1.5  text {* Conversion from and to indices. *}
     1.6  
     1.7 -code_const index_of_nat
     1.8 +code_const Code_Index.of_nat
     1.9    (SML "IntInf.toInt")
    1.10    (OCaml "Big'_int.int'_of'_big'_int")
    1.11    (Haskell "fromEnum")
    1.12  
    1.13 -code_const nat_of_index
    1.14 +code_const Code_Index.nat_of
    1.15    (SML "IntInf.fromInt")
    1.16    (OCaml "Big'_int.big'_int'_of'_int")
    1.17    (Haskell "toEnum")