diff -r 5eb3df798405 -r f0d901bc0686 src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Mon Jan 23 14:06:40 2006 +0100
+++ b/src/HOL/Library/EfficientNat.thy	Mon Jan 23 14:07:52 2006 +0100
@@ -52,12 +52,12 @@
   int ("(_)")
 
 (* code_syntax_tyco nat
-  ml (atom "InfInt.int")
-  haskell (atom "Integer")
+  ml (target_atom "InfInt.int")
+  haskell (target_atom "Integer")
 
 code_syntax_const 0 :: nat
   ml ("0 : InfInt.int")
-  haskell (atom "0")
+  haskell (target_atom "0")
 
 code_syntax_const Suc
   ml (infixl 8 "_ + 1")