src/HOL/Tools/numeral.ML
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