--- a/src/Pure/ML/ml_pp.ML Fri Sep 06 13:49:43 2024 +0200
+++ b/src/Pure/ML/ml_pp.ML Fri Sep 06 13:57:06 2024 +0200
@@ -79,7 +79,7 @@
fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
fun prt_term parens (dp: FixedInt.int) t =
- if dp <= 0 then Pretty.str "..."
+ if dp <= 0 then Pretty.dots
else
(case t of
_ $ _ =>
@@ -98,7 +98,7 @@
| Bound a => prt_app "Bound" (Pretty.from_ML (ML_system_pretty (a, dp - 1))));
fun prt_proof parens dp prf =
- if dp <= 0 then Pretty.str "..."
+ if dp <= 0 then Pretty.dots
else
(case prf of
_ % _ => prt_proofs parens dp prf