diff -r d682b4000a77 -r f8e52c0152fe src/HOL/Tools/Sledgehammer/async_manager_legacy.ML
--- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Sat Apr 04 21:38:20 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Sun Apr 05 13:05:40 2020 +0200
@@ -24,7 +24,7 @@
       Runtime.debugging NONE body () handle exn =>
         if Exn.is_interrupt exn then ()
         else writeln ("## INTERNAL ERROR ##\n" ^ Runtime.exn_message exn),
-      Standard_Thread.attributes
+      Isabelle_Thread.attributes
         {name = "async_manager", stack_limit = NONE, interrupts = interrupts});
 
 fun implode_message (workers, work) =
@@ -108,7 +108,7 @@
               NONE
             else
               let
-                val _ = List.app (Standard_Thread.interrupt_unsynchronized o #1) canceling
+                val _ = List.app (Isabelle_Thread.interrupt_unsynchronized o #1) canceling
                 val canceling' = filter (Thread.isActive o #1) canceling
                 val state' = make_state manager timeout_heap' active canceling' messages
               in SOME (map #2 timeout_threads, state') end