1.1 --- a/src/HOL/Code_Numeral.thy	Fri Jan 22 13:38:28 2010 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Fri Jan 22 13:38:28 2010 +0100
     1.3 @@ -296,15 +296,14 @@
     1.4  
     1.5  setup {*
     1.6    fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
     1.7 -    false false Code_Printer.str) ["SML", "Haskell"]
     1.8 +    false Code_Printer.literal_naive_numeral) ["SML", "Haskell"]
     1.9    #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.10 -    false true Code_Printer.str "OCaml"
    1.11 +    false Code_Printer.literal_numeral "OCaml"
    1.12    #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.13 -    false false Code_Printer.str "Scala"
    1.14 +    false Code_Printer.literal_naive_numeral "Scala"
    1.15  *}
    1.16  
    1.17  code_reserved SML Int int
    1.18 -code_reserved OCaml Big_int
    1.19  code_reserved Scala Int
    1.20  
    1.21  code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"