--- a/src/HOL/Tools/numeral.ML Fri Jan 22 13:38:28 2010 +0100
+++ b/src/HOL/Tools/numeral.ML Fri Jan 22 13:38:28 2010 +0100
@@ -8,7 +8,7 @@
sig
val mk_cnumeral: int -> cterm
val mk_cnumber: ctyp -> int -> cterm
- val add_code: string -> bool -> bool -> (string -> Pretty.T) -> string -> theory -> theory
+ val add_code: string -> bool -> (Code_Printer.literals -> int -> string) -> string -> theory -> theory
end;
structure Numeral: NUMERAL =
@@ -56,7 +56,7 @@
local open Basic_Code_Thingol in
-fun add_code number_of negative unbounded print target thy =
+fun add_code number_of negative print target thy =
let
fun dest_numeral pls' min' bit0' bit1' thm =
let
@@ -74,8 +74,7 @@
| dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
in dest_num end;
fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] =
- (print o Code_Printer.literal_numeral literals unbounded
- o the_default 0 o dest_numeral 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
(SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min},