| changeset 80809 | 4a64fc4d1cde |
| parent 80803 | 7e39c785ca5d |
| child 80820 | db114ec720cb |
--- a/src/Pure/PIDE/xml.ML Wed Sep 04 16:21:52 2024 +0200 +++ b/src/Pure/PIDE/xml.ML Thu Sep 05 17:39:45 2024 +0200 @@ -171,7 +171,7 @@ fun pretty depth tree = Pretty.str (content_depth (Int.max (0, depth)) tree); -val _ = ML_system_pp (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth)); +val _ = ML_system_pp (fn depth => fn _ => Pretty.to_ML o pretty (FixedInt.toInt depth));