changeset 25967 | dd602eb20f3f |
parent 25932 | db0fd0ecdcd4 |
child 26086 | 3c243098b64a |
--- a/src/HOL/Tools/numeral.ML Fri Jan 25 14:54:44 2008 +0100 +++ b/src/HOL/Tools/numeral.ML Fri Jan 25 14:54:46 2008 +0100 @@ -56,7 +56,7 @@ (* code generator *) fun add_code number_of negative unbounded target = - CodeTarget.add_pretty_numeral target unbounded negative number_of + CodeTarget.add_pretty_numeral target negative unbounded number_of @{const_name Int.B0} @{const_name Int.B1} @{const_name Int.Pls} @{const_name Int.Min} @{const_name Int.Bit};