diff -r 4356b52b03f7 -r a48f9ef9de15 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Tue Jun 02 15:53:04 2009 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jun 02 15:53:05 2009 +0200
@@ -371,12 +371,12 @@
 
 code_const Code_Numeral.of_nat
   (SML "IntInf.toInt")
-  (OCaml "Big'_int.int'_of'_big'_int")
+  (OCaml "_")
   (Haskell "fromEnum")
 
 code_const Code_Numeral.nat_of
   (SML "IntInf.fromInt")
-  (OCaml "Big'_int.big'_int'_of'_int")
+  (OCaml "_")
   (Haskell "toEnum")
 
 text {* Using target language arithmetic operations whenever appropriate *}