--- a/src/Pure/Thy/thy_info.ML Tue Nov 18 18:25:55 2008 +0100
+++ b/src/Pure/Thy/thy_info.ML Tue Nov 18 18:25:59 2008 +0100
@@ -326,7 +326,9 @@
val deps = map_filter (Symtab.lookup tab) (Graph.imm_preds task_graph name);
val x = Future.future (SOME group) deps true body;
in (x, Symtab.update (name, Future.task_of x) tab) end;
- in ignore (Exn.release_all (Future.join_results (#1 (fold_map future tasks Symtab.empty)))) end;
+ val _ = ignore (Exn.release_all (Future.join_results (#1 (fold_map future tasks Symtab.empty))));
+ val _ = List.app (PureThy.force_proofs o get_theory o #1) tasks;
+ in () end;
local
@@ -587,12 +589,8 @@
(* finish all theories *)
-fun force_proofs thy =
- Facts.dest_static (map PureThy.facts_of (Theory.parents_of thy)) (PureThy.facts_of thy)
- |> maps #2 |> ParList.map Thm.proof_of;
-
fun finish () = change_thys (Graph.map_nodes
- (fn (SOME _, SOME thy) => (NONE, (force_proofs thy; SOME thy))
+ (fn (SOME _, SOME thy) => (NONE, (PureThy.force_proofs thy; SOME thy))
| (_, entry) => (NONE, entry)));
end;