# 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));