diff -r 6e9a47d3850c -r 5b49c650d413 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Jun 07 09:27:01 2021 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon Jun 07 09:36:21 2021 +0200
@@ -197,6 +197,12 @@
 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
@@ -212,10 +218,7 @@
       | 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
@@ -251,6 +254,8 @@
     val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
   in Par_Exn.release_all present_results end);
 
+end;
+
 
 (* eval theory *)