diff -r 3533485fc7b8 -r d4a6460c53d1 src/HOL/Tools/numeral.ML
--- a/src/HOL/Tools/numeral.ML	Fri Aug 29 20:36:08 2008 +0200
+++ b/src/HOL/Tools/numeral.ML	Mon Sep 01 10:18:37 2008 +0200
@@ -56,7 +56,7 @@
 (* code generator *)
 
 fun add_code number_of negative unbounded target =
-  Code_Target.add_pretty_numeral target negative unbounded number_of
+  Code_Target.add_literal_numeral target negative unbounded number_of
   @{const_name Int.Pls} @{const_name Int.Min}
   @{const_name Int.Bit0} @{const_name Int.Bit1};