# HG changeset patch
# User wenzelm
# Date 1228518512 -3600
# Node ID c9cdb569487a4dc05eefbee36e4a6d965b772df8
# Parent  b97a3f80813318dcaae4d0d2671b8ae6d2bc2e8f
renamed force_proofs to join_proofs;

diff -r b97a3f808133 -r c9cdb569487a src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sat Dec 06 00:08:07 2008 +0100
+++ b/src/Pure/pure_thy.ML	Sat Dec 06 00:08:32 2008 +0100
@@ -11,7 +11,7 @@
   val intern_fact: theory -> xstring -> string
   val defined_fact: theory -> string -> bool
   val hide_fact: bool -> string -> theory -> theory
-  val force_proofs: theory -> unit
+  val join_proofs: theory list -> unit Exn.result list
   val get_fact: Context.generic -> theory -> Facts.ref -> thm list
   val get_thms: theory -> xstring -> thm list
   val get_thm: theory -> xstring -> thm
@@ -79,10 +79,9 @@
 
 (* proofs *)
 
-fun lazy_proof thm = Lazy.lazy (fn () => Thm.force_proof thm);
+fun lazy_proof thm = Lazy.lazy (fn () => Thm.join_proof thm);
 
-fun force_proofs thy =
-  ignore (Exn.release_all (map (Exn.capture Lazy.force) (rev (#2 (FactsData.get thy)))));
+val join_proofs = maps (fn thy => map (Exn.capture Lazy.force) (rev (#2 (FactsData.get thy))));