src/HOL/Tools/numeral.ML
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,