changeset 28064 | d4a6460c53d1 |
parent 28054 | 2b84d34c5d02 |
child 28090 | 29af3c712d2b |
1.1 --- a/src/HOL/Tools/numeral.ML Fri Aug 29 20:36:08 2008 +0200 1.2 +++ b/src/HOL/Tools/numeral.ML Mon Sep 01 10:18:37 2008 +0200 1.3 @@ -56,7 +56,7 @@ 1.4 (* code generator *) 1.5 1.6 fun add_code number_of negative unbounded target = 1.7 - Code_Target.add_pretty_numeral target negative unbounded number_of 1.8 + Code_Target.add_literal_numeral target negative unbounded number_of 1.9 @{const_name Int.Pls} @{const_name Int.Min} 1.10 @{const_name Int.Bit0} @{const_name Int.Bit1}; 1.11