--- a/src/HOL/Tools/numeral.ML Tue Aug 31 13:15:35 2010 +0200
+++ b/src/HOL/Tools/numeral.ML Tue Aug 31 13:29:38 2010 +0200
@@ -76,7 +76,7 @@
fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] =
(Code_Printer.str o print literals o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
in
- thy |> Code_Target.add_syntax_const target number_of
+ thy |> Code_Target.add_const_syntax target number_of
(SOME (Code_Printer.complex_const_syntax (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
@{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty))))
end;