src/HOL/Code_Numeral.thy
changeset 58399 c5430cf9aa87
parent 58390 b74d8470b98e
child 58400 d0d3c30806b4
     1.1 --- a/src/HOL/Code_Numeral.thy	Thu Sep 18 18:48:04 2014 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Thu Sep 18 18:48:04 2014 +0200
     1.3 @@ -544,13 +544,10 @@
     1.4      and (Scala) "BigInt(0)"
     1.5  
     1.6  setup {*
     1.7 -  fold (Numeral.add_code @{const_name Code_Numeral.Pos}
     1.8 -    false Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
     1.9 -*}
    1.10 -
    1.11 -setup {*
    1.12 -  fold (Numeral.add_code @{const_name Code_Numeral.Neg}
    1.13 -    true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
    1.14 +  fold (fn target =>
    1.15 +    Numeral.add_code @{const_name Code_Numeral.Pos} I Code_Printer.literal_numeral target
    1.16 +    #> Numeral.add_code @{const_name Code_Numeral.Neg} (op ~) Code_Printer.literal_numeral target)
    1.17 +    ["SML", "OCaml", "Haskell", "Scala"]
    1.18  *}
    1.19  
    1.20  code_printing