src/Pure/Concurrent/future.ML
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)));