# HG changeset patch
# User wenzelm
# Date 1231547298 -3600
# Node ID 75ac4d6ff8fb64e9aa74779845ee64b767070060
# Parent  fdf396a24a9f31f8696749e242222ea8545f5b9d
tuned;

diff -r fdf396a24a9f -r 75ac4d6ff8fb src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sat Jan 10 01:28:03 2009 +0100
+++ b/src/Pure/pure_thy.ML	Sat Jan 10 01:28:18 2009 +0100
@@ -81,8 +81,7 @@
 fun lazy_proof thm = Lazy.lazy (fn () => Thm.join_proof thm);
 
 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));
+  map_filter (Exn.get_exn o Lazy.force_result) (rev (#2 (FactsData.get thy)));