diff -r b73678836f8e -r 6fb85346cb79 src/Pure/ML/ml_compiler.ML --- 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}