diff -r 3b9ca8d2c5fb -r 096c8397c989 src/HOL/Tools/numeral.ML --- a/src/HOL/Tools/numeral.ML Mon Jul 19 11:55:43 2010 +0200 +++ b/src/HOL/Tools/numeral.ML Mon Jul 19 11:55:44 2010 +0200 @@ -77,8 +77,8 @@ (Code_Printer.str o print literals o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t; in thy |> Code_Target.add_syntax_const target number_of - (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min}, - @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty))) + (SOME (Code_Printer.complex_const_syntax (1, ([@{const_name Int.Pls}, @{const_name Int.Min}, + @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))) end; end; (*local*)