src/Pure/Thy/thy_info.ML

     commit = I};
 
 fun result_theory (Result {theory, ...}) = theory;
 fun result_commit (Result {commit, ...}) = commit;
 
+datatype task =
+  Task of string list * (theory list -> result) |
+  Finished of theory;
+
+local
+
 fun consolidate_theory (Exn.Exn exn) = [Exn.Exn exn]
   | consolidate_theory (Exn.Res (Result {theory, exec_id, ...})) =
       let
         val _ = Execution.join [exec_id];
         val res = Exn.capture Thm.consolidate_theory theory;

       (case present () of
         NONE => []
       | SOME (context as {segments, ...}) =>
           [Exn.capture (fn () => (apply_presentation context theory; (theory, segments))) ()]);
 
-
-datatype task =
-  Task of string list * (theory list -> result) |
-  Finished of theory;
+in
 
 val schedule_theories = Thread_Attributes.uninterruptible (fn _ => fn tasks =>
   let
     fun join_parents deps name parents =
       (case map #1 (filter (not o can Future.join o #2) deps) of

     val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ()));
 
     val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
   in Par_Exn.release_all present_results end);
 
+end;
+
 
 (* eval theory *)
 
 fun eval_thy options master_dir header text_pos text parents =
   let