src/HOL/Library/Code_Target_Nat.thy
changeset 52435 6646bb548c6b
parent 51143 0a2371e7ced3
child 53027 1774d569b604
--- a/src/HOL/Library/Code_Target_Nat.thy	Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Library/Code_Target_Nat.thy	Sun Jun 23 21:16:07 2013 +0200
@@ -123,14 +123,9 @@
   "integer_of_nat (nat k) = max 0 (integer_of_int k)"
   by transfer auto
 
-code_modulename SML
-  Code_Target_Nat Arith
-
-code_modulename OCaml
-  Code_Target_Nat Arith
-
-code_modulename Haskell
-  Code_Target_Nat Arith
+code_identifier
+  code_module Code_Target_Nat \<rightharpoonup>
+    (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
 end