src/Pure/Thy/thy_info.ML

     val tasks = Graph.minimals G |> map (fn name =>
       (name, (Graph.get_node G name, length (Graph.imm_succs G name))));
     val finished = filter (task_finished o fst o snd) tasks;
   in
     if not (null finished) then next_task (Graph.del_nodes (map fst finished) G)
-    else if null tasks then (Multithreading.Terminate, G)
+    else if null tasks then (Schedule.Terminate, G)
     else
       (case fold max_task tasks NONE of
-        NONE => (Multithreading.Wait, G)
+        NONE => (Schedule.Wait, G)
       | SOME (name, (body, _)) =>
-         (Multithreading.Task {body = PrintMode.closure body,
+         (Schedule.Task {body = PrintMode.closure body,
            cont = Graph.del_nodes [name], fail = K Graph.empty},
           Graph.map_node name (K Running) G))
   end;
 
 fun schedule_seq tasks =

     if m <= 1 orelse n <= 1 then schedule_seq tasks
     else if Multithreading.self_critical () then
      (warning (loader_msg "no multithreading within critical section" []);
       schedule_seq tasks)
     else
-      (case Multithreading.schedule (Int.min (m, n)) next_task tasks of
+      (case Schedule.schedule (Int.min (m, n)) next_task tasks of
         [] => ()
       | exns => raise Exn.EXCEPTIONS (exns, ""))
   end;
 
 end;