src/Pure/Concurrent/task_queue.ML
changeset 62819 d3ff367a16a0
parent 62663 bea354f6ff21
child 62826 eb94e570c1a4
--- a/src/Pure/Concurrent/task_queue.ML	Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Sat Apr 02 21:10:07 2016 +0200
@@ -397,7 +397,7 @@
 
 (* toplevel pretty printing *)
 
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_task);
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_group);
+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);
 
 end;