src/Pure/Thy/thy_info.ML

     | Finished thy => Symtab.update (name, thy) tab))) |> ignore;
 
 fun schedule_futures task_graph = uninterruptible (fn _ => fn () =>
   let
     val tasks = Graph.topological_order task_graph;
-    val par_proofs = ! parallel_proofs >= 1;
-
     val futures = (tasks, Symtab.empty) |-> fold (fn name => fn tab =>
       (case Graph.get_node task_graph name of
         Task (parents, body) =>
           let
             val get = the o Symtab.lookup tab;

             val future = Future.fork_deps (map #1 deps) (fn () =>
               (case map_filter failed deps of
                 [] => body (map (#1 o Future.join o get) parents)
               | bad => error (loader_msg
                   ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") [])));
-            val future' =
-              if par_proofs then future
-              else Future.map (fn (thy, after_load) => (after_load (); (thy, I))) future;
-          in Symtab.update (name, future') tab end
+          in Symtab.update (name, future) tab end
       | Finished thy => Symtab.update (name, Future.value (thy, I)) tab));
-
     val _ =
       tasks |> maps (fn name =>
         let
           val (thy, after_load) = Future.join (the (Symtab.lookup futures name));
           val _ = PureThy.join_proofs thy;