src/HOL/Tools/Sledgehammer/sledgehammer.ML

                         signed_string_of_int (Time.toMilliseconds
                             (Timer.checkRealTimer timer)) ^ " ms.")
             else
               ()
           end
-      in if blocking then run () else Toplevel.thread true (tap run) |> K () end
+      in if blocking then run () else Future.fork run |> K () end
 
 val setup =
   dest_dir_setup
   #> problem_prefix_setup
   #> measure_run_time_setup