src/HOL/Code_Numeral.thy
changeset 69593 3dda49e08b9d
parent 68028 1f9f973eed2a
child 69906 55534affe445
     1.1 --- a/src/HOL/Code_Numeral.thy	Fri Jan 04 21:49:06 2019 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Fri Jan 04 23:22:53 2019 +0100
     1.3 @@ -668,8 +668,8 @@
     1.4  
     1.5  setup \<open>
     1.6    fold (fn target =>
     1.7 -    Numeral.add_code @{const_name Code_Numeral.Pos} I Code_Printer.literal_numeral target
     1.8 -    #> Numeral.add_code @{const_name Code_Numeral.Neg} (~) Code_Printer.literal_numeral target)
     1.9 +    Numeral.add_code \<^const_name>\<open>Code_Numeral.Pos\<close> I Code_Printer.literal_numeral target
    1.10 +    #> Numeral.add_code \<^const_name>\<open>Code_Numeral.Neg\<close> (~) Code_Printer.literal_numeral target)
    1.11      ["SML", "OCaml", "Haskell", "Scala"]
    1.12  \<close>
    1.13