diff -r be3c0df7bb90 -r 844977c7abeb src/HOL/Library/Efficient_Nat.thy --- a/src/HOL/Library/Efficient_Nat.thy Fri Jul 23 10:25:00 2010 +0200 +++ b/src/HOL/Library/Efficient_Nat.thy Fri Jul 23 10:58:13 2010 +0200 @@ -412,13 +412,13 @@ code_const Code_Numeral.of_nat (SML "IntInf.toInt") (OCaml "_") - (Haskell "fromEnum") + (Haskell "toInteger") (Scala "!_.as'_Int") code_const Code_Numeral.nat_of (SML "IntInf.fromInt") (OCaml "_") - (Haskell "toEnum") + (Haskell "fromInteger") (Scala "Nat") text {* Using target language arithmetic operations whenever appropriate *}