src/Pure/thm.ML

   val freezeT: thm -> thm
   val join_futures: theory -> unit
   val future: (unit -> thm) -> cterm -> thm
   val proof_body_of: thm -> proof_body
   val proof_of: thm -> proof
+  val force_proof: thm -> unit
   val extern_oracles: theory -> xstring list
   val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
 end;
 
 structure Thm:> THM =

 
 structure Futures = TheoryDataFun
 (
   type T = thm Future.T list ref;
   val empty : T = ref [];
-  val copy = I;  (*shared ref within whole theory body*)
+  val copy = I;  (*shared ref within all versions of whole theory body*)
   fun extend _ : T = ref [];
   fun merge _ _ : T = ref [];
 );
 
 val _ = Context.>> (Context.map_theory Futures.init);

       CRITICAL (fn () =>
         let
           val (finished, unfinished) = List.partition Future.is_finished (! futures);
           val _ = futures := unfinished;
         in finished end)
-      |> Future.join_results |> Exn.release_all |> null);
+      |> Future.join_results |> null);
   in while not (joined ()) do () end;
 
 
 (* future rule *)
 

     val _ = Exn.release_all (map (Future.join_result o #2) (rev all_promises));
     val ps = map (apsnd (Lazy.value o raw_proof_of o Future.join)) promises;
   in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
 
 val proof_of = Proofterm.proof_of o proof_body_of;
+val force_proof = ignore o proof_body_of;
 
 
 (* closed derivations with official name *)
 
 fun get_name thm =