--- a/src/Pure/Thy/thy_info.ML Thu Sep 04 16:03:48 2008 +0200
+++ b/src/Pure/Thy/thy_info.ML Thu Sep 04 16:03:49 2008 +0200
@@ -329,12 +329,12 @@
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;
@@ -352,7 +352,7 @@
(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;