changeset 29423 | 75ac4d6ff8fb |
parent 29420 | b28bf19d7ab9 |
child 29433 | c42620170fa6 |
--- 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)));