changeset 82380 | ceb4f33d3073 |
parent 77879 | dd222e2af01a |
--- a/src/HOL/Tools/numeral.ML Sun Mar 30 13:50:06 2025 +0200 +++ b/src/HOL/Tools/numeral.ML Sun Mar 30 13:50:06 2025 +0200 @@ -104,7 +104,7 @@ let fun pretty literals _ thm _ _ [(t, _)] = case dest_num_code t of - SOME n => (Code_Printer.str o print literals o preproc) n + SOME n => (Pretty.str o print literals o preproc) n | NONE => Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal term"; in thy |> Code_Target.set_printings (Code_Symbol.Constant (number_of,