src/Pure/Concurrent/task_queue.ML
changeset 80809 4a64fc4d1cde
parent 79446 ec7a1603129a
--- a/src/Pure/Concurrent/task_queue.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -430,7 +430,7 @@
 
 (* toplevel pretty printing *)
 
-val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_task);
-val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_group);
+val _ = ML_system_pp (fn _ => fn _ => ML_Pretty.str o str_of_task);
+val _ = ML_system_pp (fn _ => fn _ => ML_Pretty.str o str_of_group);
 
 end;