1.1 --- a/src/Pure/pure_thy.ML	Sat Dec 06 00:08:07 2008 +0100
     1.2 +++ b/src/Pure/pure_thy.ML	Sat Dec 06 00:08:32 2008 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4    val intern_fact: theory -> xstring -> string
     1.5    val defined_fact: theory -> string -> bool
     1.6    val hide_fact: bool -> string -> theory -> theory
     1.7 -  val force_proofs: theory -> unit
     1.8 +  val join_proofs: theory list -> unit Exn.result list
     1.9    val get_fact: Context.generic -> theory -> Facts.ref -> thm list
    1.10    val get_thms: theory -> xstring -> thm list
    1.11    val get_thm: theory -> xstring -> thm
    1.12 @@ -79,10 +79,9 @@
    1.13  
    1.14  (* proofs *)
    1.15  
    1.16 -fun lazy_proof thm = Lazy.lazy (fn () => Thm.force_proof thm);
    1.17 +fun lazy_proof thm = Lazy.lazy (fn () => Thm.join_proof thm);
    1.18  
    1.19 -fun force_proofs thy =
    1.20 -  ignore (Exn.release_all (map (Exn.capture Lazy.force) (rev (#2 (FactsData.get thy)))));
    1.21 +val join_proofs = maps (fn thy => map (Exn.capture Lazy.force) (rev (#2 (FactsData.get thy))));
    1.22  
    1.23  
    1.24