src/HOL/Library/Efficient_Nat.thy
changeset 37947 844977c7abeb
parent 37892 3d8857f42a64
child 37958 9728342bcd56
--- 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 *}