src/Pure/ML/ml_compiler.ML
changeset 68130 6fb85346cb79
parent 67362 221612c942de
child 68816 5a53724fe247
--- a/src/Pure/ML/ml_compiler.ML	Wed May 09 19:53:37 2018 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Wed May 09 20:45:57 2018 +0200
@@ -120,7 +120,7 @@
       |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
       |> Output.report;
     val _ =
-      if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
+      if not (null persistent_reports) andalso redirect andalso Future.enabled ()
       then
         Execution.print
           {name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri}