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*)