diff -r a80d8ec6c998 -r 3dda49e08b9d src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Fri Jan 04 21:49:06 2019 +0100 +++ b/src/HOL/Code_Numeral.thy Fri Jan 04 23:22:53 2019 +0100 @@ -668,8 +668,8 @@ setup \ 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} (~) Code_Printer.literal_numeral target) + Numeral.add_code \<^const_name>\Code_Numeral.Pos\ I Code_Printer.literal_numeral target + #> Numeral.add_code \<^const_name>\Code_Numeral.Neg\ (~) Code_Printer.literal_numeral target) ["SML", "OCaml", "Haskell", "Scala"] \