--- a/src/HOL/Tools/numeral.ML Wed Jan 13 12:20:37 2010 +0100
+++ b/src/HOL/Tools/numeral.ML Thu Jan 14 17:47:38 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 -> theory -> theory
+ val add_code: string -> bool -> bool -> (string -> Pretty.T) -> string -> theory -> theory
end;
structure Numeral: NUMERAL =
@@ -56,7 +56,7 @@
local open Basic_Code_Thingol in
-fun add_code number_of negative unbounded target thy =
+fun add_code number_of negative unbounded print target thy =
let
fun dest_numeral pls' min' bit0' bit1' thm =
let
@@ -74,11 +74,12 @@
| 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, _)] =
- (Code_Printer.str o Code_Printer.literal_numeral literals unbounded
+ (print o Code_Printer.literal_numeral literals unbounded
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}, @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))
+ (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
+ @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))
end;
end; (*local*)