diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/Concurrent/task_queue.ML --- 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;