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 type Lazy.T to lazy;
authorwenzelm
Thu, 04 Dec 2008 23:02:52 +0100
changeset 28977 08990d02211f
parent 28976 53c96f58e38f
child 28978 f3e37d78b4f7
renamed type Lazy.T to lazy; force_proofs: original order;
src/Pure/pure_thy.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/pure_thy.ML	Thu Dec 04 23:02:46 2008 +0100
+++ b/src/Pure/pure_thy.ML	Thu Dec 04 23:02:52 2008 +0100
@@ -59,7 +59,7 @@
 
 structure FactsData = TheoryDataFun
 (
-  type T = Facts.T * unit Lazy.T list;
+  type T = Facts.T * unit lazy list;
   val empty = (Facts.empty, []);
   val copy = I;
   fun extend (facts, _) = (facts, []);
@@ -80,7 +80,9 @@
 (* proofs *)
 
 fun lazy_proof thm = Lazy.lazy (fn () => Thm.force_proof thm);
-val force_proofs = List.app Lazy.force o #2 o FactsData.get;
+
+fun force_proofs thy =
+  ignore (Exn.release_all (map (Exn.capture Lazy.force) (rev (#2 (FactsData.get thy)))));
isabelle