Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
renamed force_proofs to join_proofs;
authorwenzelm
Sat, 06 Dec 2008 00:08:32 +0100
changeset 29002 c9cdb569487a
parent 29001 b97a3f808133
child 29003 d8d3cbbb6fcc
renamed force_proofs to join_proofs;
src/Pure/pure_thy.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/pure_thy.ML	Sat Dec 06 00:08:07 2008 +0100
+++ b/src/Pure/pure_thy.ML	Sat Dec 06 00:08:32 2008 +0100
@@ -11,7 +11,7 @@
   val intern_fact: theory -> xstring -> string
   val defined_fact: theory -> string -> bool
   val hide_fact: bool -> string -> theory -> theory
-  val force_proofs: theory -> unit
+  val join_proofs: theory list -> unit Exn.result list
   val get_fact: Context.generic -> theory -> Facts.ref -> thm list
   val get_thms: theory -> xstring -> thm list
   val get_thm: theory -> xstring -> thm
@@ -79,10 +79,9 @@
 
 (* proofs *)
 
-fun lazy_proof thm = Lazy.lazy (fn () => Thm.force_proof thm);
+fun lazy_proof thm = Lazy.lazy (fn () => Thm.join_proof thm);
 
-fun force_proofs thy =
-  ignore (Exn.release_all (map (Exn.capture Lazy.force) (rev (#2 (FactsData.get thy)))));
+val join_proofs = maps (fn thy => map (Exn.capture Lazy.force) (rev (#2 (FactsData.get thy))));
isabelle