# HG changeset patch
# User wenzelm
# Date 1502098472 -7200
# Node ID 26735fab7a8f965c56d9d351618624a717332394
# Parent  b60afdf1177d0a6b4ee3a375c9b916e4cdab82e9
tuned;

diff -r b60afdf1177d -r 26735fab7a8f src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Aug 07 11:20:19 2017 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon Aug 07 11:34:32 2017 +0200
@@ -169,8 +169,6 @@
 
 fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents;
 
-local
-
 val schedule_seq =
   String_Graph.schedule (fn deps => fn (_, task) =>
     (case task of
@@ -222,13 +220,6 @@
     val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
   in () end);
 
-in
-
-fun schedule_tasks tasks =
-  if Multithreading.enabled () then schedule_futures tasks else schedule_seq tasks;
-
-end;
-
 
 (* eval theory *)
 
@@ -403,7 +394,7 @@
   let
     val (_, tasks) =
       require_thys document symbols last_timing [] qualifier master_dir imports String_Graph.empty;
-  in schedule_tasks tasks end;
+  in if Multithreading.enabled () then schedule_futures tasks else schedule_seq tasks end;
 
 fun use_thy name =
   use_theories