src/Pure/ML/ml_pp.ML
changeset 79127 830f68f92ad7
parent 78649 d46006355819
child 80803 7e39c785ca5d
--- 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