diff -r 4a64fc4d1cde -r 1f718be3608b src/Pure/ML/ml_pp.ML
--- a/src/Pure/ML/ml_pp.ML	Thu Sep 05 17:39:45 2024 +0200
+++ b/src/Pure/ML/ml_pp.ML	Thu Sep 05 21:16:53 2024 +0200
@@ -25,19 +25,19 @@
   ML_system_pp (fn _ => fn _ => Pretty.to_ML o Proof_Display.pp_context);
 
 val _ =
-  ML_system_pp (fn depth => fn _ => Pretty.prune_ML depth o Proof_Display.pp_thm);
+  ML_system_pp (fn depth => fn _ => ML_Pretty.prune depth o Pretty.to_ML o Proof_Display.pp_thm);
 
 val _ =
-  ML_system_pp (fn depth => fn _ => Pretty.prune_ML depth o Proof_Display.pp_cterm);
+  ML_system_pp (fn depth => fn _ => ML_Pretty.prune depth o Pretty.to_ML o Proof_Display.pp_cterm);
 
 val _ =
-  ML_system_pp (fn depth => fn _ => Pretty.prune_ML depth o Proof_Display.pp_ctyp);
+  ML_system_pp (fn depth => fn _ => ML_Pretty.prune depth o Pretty.to_ML o Proof_Display.pp_ctyp);
 
 val _ =
-  ML_system_pp (fn depth => fn _ => Pretty.prune_ML depth o Proof_Display.pp_typ);
+  ML_system_pp (fn depth => fn _ => ML_Pretty.prune depth o Pretty.to_ML o Proof_Display.pp_typ);
 
 val _ =
-  ML_system_pp (fn depth => fn _ => Pretty.prune_ML depth o Proof_Display.pp_ztyp);
+  ML_system_pp (fn depth => fn _ => ML_Pretty.prune depth o Pretty.to_ML o Proof_Display.pp_ztyp);
 
 
 local