diff -r bdb33a2d4167 -r 830f68f92ad7 src/Pure/ML/ml_pp.ML
--- a/src/Pure/ML/ml_pp.ML	Tue Dec 05 11:02:05 2023 +0100
+++ b/src/Pure/ML/ml_pp.ML	Tue Dec 05 11:11:00 2023 +0100
@@ -31,6 +31,10 @@
   ML_system_pp (fn depth => fn _ =>
     ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Theory.get_pure);
 
+val _ =
+  ML_system_pp (fn depth => fn _ =>
+    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_ztyp Theory.get_pure);
+
 
 local