1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue May 19 13:57:51 2009 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue May 19 16:54:55 2009 +0200
     1.3 @@ -369,12 +369,12 @@
     1.4  
     1.5  text {* Conversion from and to indices. *}
     1.6  
     1.7 -code_const Code_Index.of_nat
     1.8 +code_const Code_Numeral.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 Code_Index.nat_of
    1.14 +code_const Code_Numeral.nat_of
    1.15    (SML "IntInf.fromInt")
    1.16    (OCaml "Big'_int.big'_int'_of'_int")
    1.17    (Haskell "toEnum")