--- 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