changeset 80809 | 4a64fc4d1cde |
parent 78787 | a7e4b412cc7c |
--- a/src/Pure/Concurrent/future.ML Wed Sep 04 16:21:52 2024 +0200 +++ b/src/Pure/Concurrent/future.ML Thu Sep 05 17:39:45 2024 +0200 @@ -111,8 +111,8 @@ val _ = ML_system_pp (fn depth => fn pretty => fn x => (case peek x of - NONE => PolyML.PrettyString "<future>" - | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" + NONE => ML_Pretty.str "<future>" + | SOME (Exn.Exn _) => ML_Pretty.str "<failed>" | SOME (Exn.Res y) => pretty (y, depth)));