src/HOL/Tools/numeral.ML
changeset 28054 2b84d34c5d02
parent 26086 3c243098b64a
child 28064 d4a6460c53d1
--- a/src/HOL/Tools/numeral.ML	Thu Aug 28 22:08:11 2008 +0200
+++ b/src/HOL/Tools/numeral.ML	Thu Aug 28 22:09:20 2008 +0200
@@ -56,7 +56,7 @@
 (* code generator *)
 
 fun add_code number_of negative unbounded target =
-  CodeTarget.add_pretty_numeral target negative unbounded number_of
+  Code_Target.add_pretty_numeral target negative unbounded number_of
   @{const_name Int.Pls} @{const_name Int.Min}
   @{const_name Int.Bit0} @{const_name Int.Bit1};