src/HOL/Tools/Sledgehammer/async_manager_legacy.ML

--- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Mon Sep 04 21:03:13 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Wed Sep 06 14:09:27 2023 +0200
@@ -26,21 +26,21 @@
 
 structure Thread_Heap = Heap
 (
-  type elem = Time.time * Thread.thread
+  type elem = Time.time * Isabelle_Thread.T
   fun ord ((a, _), (b, _)) = Time.compare (a, b)
 )
 
-fun lookup_thread xs = AList.lookup Thread.equal xs
-fun delete_thread xs = AList.delete Thread.equal xs
-fun update_thread xs = AList.update Thread.equal xs
+fun lookup_thread xs = AList.lookup Isabelle_Thread.equal xs
+fun delete_thread xs = AList.delete Isabelle_Thread.equal xs
+fun update_thread xs = AList.update Isabelle_Thread.equal xs
 
 type state =
-  {manager: Thread.thread option,
+  {manager: Isabelle_Thread.T option,
    timeout_heap: Thread_Heap.T,
    active:
-     (Thread.thread
+     (Isabelle_Thread.T
       * (string * Time.time * Time.time * (string * string))) list,
-   canceling:  (Thread.thread * (string * Time.time * (string * string))) list,
+   canceling:  (Isabelle_Thread.T * (string * Time.time * (string * string))) list,
    messages: (bool * (string * (string * string))) list}
 
 fun make_state manager timeout_heap active canceling messages : state =
@@ -85,7 +85,7 @@
 
 fun check_thread_manager () = Synchronized.change global_state
   (fn state as {manager, timeout_heap, active, canceling, messages} =>
-    if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
+    if (case manager of SOME thread => Isabelle_Thread.is_active thread | NONE => false) then state
     else let val manager = SOME (make_thread false (fn () =>
       let
         fun time_limit timeout_heap =
@@ -96,14 +96,14 @@
         (*action: find threads whose timeout is reached, and interrupt canceling threads*)
         fun action {manager, timeout_heap, active, canceling, messages} =
           let val (timeout_threads, timeout_heap') =
-            Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap
+            Thread_Heap.upto (Time.now (), Isabelle_Thread.self ()) timeout_heap
           in
             if null timeout_threads andalso null canceling then
               NONE
             else
               let
                 val _ = List.app (Isabelle_Thread.interrupt_unsynchronized o #1) canceling
-                val canceling' = filter (Thread.isActive o #1) canceling
+                val canceling' = filter (Isabelle_Thread.is_active o #1) canceling
                 val state' = make_state manager timeout_heap' active canceling' messages
               in SOME (map #2 timeout_threads, state') end
           end
@@ -138,7 +138,7 @@
   (make_thread true
        (fn () =>
            let
-             val self = Thread.self ()
+             val self = Isabelle_Thread.self ()
              val _ = register tool birth_time death_time desc self
            in unregister (f ()) self end);
    ())