| changeset 28064 | d4a6460c53d1 |
| parent 28054 | 2b84d34c5d02 |
| child 28090 | 29af3c712d2b |
--- 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};