# HG changeset patch
# User wenzelm
# Date 1228428172 -3600
# Node ID 08990d02211f49018055a0709d62b608d5eb882d
# Parent  53c96f58e38f0bc686f0985e4a6a147c1fc5f18d
renamed type Lazy.T to lazy;
force_proofs: original order;

diff -r 53c96f58e38f -r 08990d02211f src/Pure/pure_thy.ML
--- 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)))));