# HG changeset patch
# User wenzelm
# Date 1231543447 -3600
# Node ID b28bf19d7ab9400de7b74d042a05def1bf373222
# Parent  8ea10ebbdc113c7711d80dd9078f25d3f040e89f
simplified join_proofs;

diff -r 8ea10ebbdc11 -r b28bf19d7ab9 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Jan 09 23:39:53 2009 +0100
+++ b/src/Pure/pure_thy.ML	Sat Jan 10 00:24:07 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/pure_thy.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Theorem storage.  Pure theory syntax and logical content.
@@ -11,7 +10,7 @@
   val intern_fact: theory -> xstring -> string
   val defined_fact: theory -> string -> bool
   val hide_fact: bool -> string -> theory -> theory
-  val join_proofs: theory list -> unit Exn.result list
+  val join_proofs: theory -> exn list
   val get_fact: Context.generic -> theory -> Facts.ref -> thm list
   val get_thms: theory -> xstring -> thm list
   val get_thm: theory -> xstring -> thm
@@ -81,7 +80,9 @@
 
 fun lazy_proof thm = Lazy.lazy (fn () => Thm.join_proof thm);
 
-val join_proofs = maps (fn thy => map (Exn.capture Lazy.force) (rev (#2 (FactsData.get thy))));
+fun join_proofs thy =
+  rev (#2 (FactsData.get thy)) |> map_filter (fn prf =>
+    (case Exn.capture Lazy.force prf of Exn.Exn exn => SOME exn | _ => NONE));