diff -r 0f820da558f9 -r 9dd4dcb08d37 src/Pure/ML/ml_pp.ML
--- 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