--- a/src/Pure/Thy/thy_info.ML Thu Sep 25 20:34:20 2008 +0200
+++ b/src/Pure/Thy/thy_info.ML Thu Sep 25 20:34:21 2008 +0200
@@ -29,7 +29,6 @@
val exec_file: bool -> Path.T -> Context.generic -> Context.generic
val use: string -> unit
val time_use: string -> unit
- val future_scheduler: bool ref
val use_thys: string list -> unit
val use_thy: string -> unit
val time_use_thy: string -> unit
@@ -316,8 +315,6 @@
datatype task = Task of (unit -> unit) | Finished | Running;
fun task_finished Finished = true | task_finished _ = false;
-val future_scheduler = ref false;
-
fun future_schedule task_graph =
let
val tasks = Graph.topological_order task_graph |> map_filter (fn name =>