diff -r be3c0df7bb90 -r 844977c7abeb src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Jul 23 10:25:00 2010 +0200
+++ b/src/HOL/Code_Numeral.thy	Fri Jul 23 10:58:13 2010 +0200
@@ -298,7 +298,7 @@
 code_type code_numeral
   (SML "int")
   (OCaml "Big'_int.big'_int")
-  (Haskell "Int")
+  (Haskell "Integer")
   (Scala "Int")
 
 code_instance code_numeral :: eq
@@ -306,11 +306,9 @@
 
 setup {*
   fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
-    false Code_Printer.literal_naive_numeral) ["SML", "Haskell"]
-  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
-    false Code_Printer.literal_numeral "OCaml"
-  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
-    false Code_Printer.literal_naive_numeral "Scala"
+    false Code_Printer.literal_naive_numeral) ["SML", "Scala"]
+  #> fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
+    false Code_Printer.literal_numeral) ["OCaml", "Haskell"]
 *}
 
 code_reserved SML Int int
@@ -325,7 +323,7 @@
 code_const "subtract_code_numeral \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   (SML "Int.max/ (_/ -/ _,/ 0 : int)")
   (OCaml "Big'_int.max'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)/ Big'_int.zero'_big'_int")
-  (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
+  (Haskell "max/ (_/ -/ _)/ (0 :: Integer)")
   (Scala "!(_/ -/ _).max(0)")
 
 code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"