--- a/src/HOL/Code_Numeral.thy Thu Sep 18 18:48:04 2014 +0200
+++ b/src/HOL/Code_Numeral.thy Thu Sep 18 18:48:04 2014 +0200
@@ -544,13 +544,10 @@
and (Scala) "BigInt(0)"
setup {*
- fold (Numeral.add_code @{const_name Code_Numeral.Pos}
- false Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
-*}
-
-setup {*
- fold (Numeral.add_code @{const_name Code_Numeral.Neg}
- true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
+ fold (fn target =>
+ Numeral.add_code @{const_name Code_Numeral.Pos} I Code_Printer.literal_numeral target
+ #> Numeral.add_code @{const_name Code_Numeral.Neg} (op ~) Code_Printer.literal_numeral target)
+ ["SML", "OCaml", "Haskell", "Scala"]
*}
code_printing