# HG changeset patch
# User wenzelm
# Date 1226963466 -3600
# Node ID 23f4928bb7e3086e0032d18120055469c21af0c9
# Parent  261bf00c6ede6d1527656cdc47d852e8d5058a48
finish: force proofs;

diff -r 261bf00c6ede -r 23f4928bb7e3 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Nov 17 23:34:35 2008 +0100
+++ b/src/Pure/Thy/thy_info.ML	Tue Nov 18 00:11:06 2008 +0100
@@ -587,6 +587,12 @@
 
 (* finish all theories *)
 
-fun finish () = change_thys (Graph.map_nodes (fn (_, entry) => (NONE, entry)));
+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))
+    | (_, entry) => (NONE, entry)));
 
 end;