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