# HG changeset patch
# User wenzelm
# Date 1222367661 -7200
# Node ID a75d4551ee008983133a78cfe0a047c5a2f53035
# Parent  6249297461cbc91b0900c76a8ac59e2345a93bfd
moved future_scheduler flag to skip_proof.ML;

diff -r 6249297461cb -r a75d4551ee00 src/Pure/Thy/thy_info.ML
--- 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 =>