# HG changeset patch
# User wenzelm
# Date 1701771060 -3600
# Node ID 830f68f92ad7ec0e1a8407cbab8c4271f205e426
# Parent  bdb33a2d4167f9478af9a42fae882de54f69213a
more ML pretty-printing;

diff -r bdb33a2d4167 -r 830f68f92ad7 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Tue Dec 05 11:02:05 2023 +0100
+++ b/src/Pure/Isar/proof_display.ML	Tue Dec 05 11:11:00 2023 +0100
@@ -12,6 +12,7 @@
   val pp_term: (unit -> theory) -> term -> Pretty.T
   val pp_ctyp: (unit -> theory) -> ctyp -> Pretty.T
   val pp_cterm: (unit -> theory) -> cterm -> Pretty.T
+  val pp_ztyp: (unit -> theory) -> ztyp -> Pretty.T
   val pretty_theory: bool -> Proof.context -> Pretty.T
   val pretty_definitions: bool -> Proof.context -> Pretty.T
   val pretty_theorems_diff: bool -> theory list -> Proof.context -> Pretty.T list
@@ -61,6 +62,8 @@
 fun pp_ctyp mk_thy cT = pp_typ mk_thy (Thm.typ_of cT);
 fun pp_cterm mk_thy ct = pp_term mk_thy (Thm.term_of ct);
 
+fun pp_ztyp mk_thy T = Pretty.quote (Syntax.pretty_typ (default_context mk_thy) (ZTerm.typ_of T));
+
 
 
 (** theory content **)
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