src/Pure/thm.ML
changeset 28842 e44fae2b721d
parent 28829 c67ab5df760b
child 28847 648f01ec1794
     1.1 --- a/src/Pure/thm.ML	Tue Nov 18 18:25:49 2008 +0100
     1.2 +++ b/src/Pure/thm.ML	Tue Nov 18 18:25:52 2008 +0100
     1.3 @@ -150,6 +150,7 @@
     1.4    val future: (unit -> thm) -> cterm -> thm
     1.5    val proof_body_of: thm -> proof_body
     1.6    val proof_of: thm -> proof
     1.7 +  val force_proof: thm -> unit
     1.8    val extern_oracles: theory -> xstring list
     1.9    val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
    1.10  end;
    1.11 @@ -1594,7 +1595,7 @@
    1.12  (
    1.13    type T = thm Future.T list ref;
    1.14    val empty : T = ref [];
    1.15 -  val copy = I;  (*shared ref within whole theory body*)
    1.16 +  val copy = I;  (*shared ref within all versions of whole theory body*)
    1.17    fun extend _ : T = ref [];
    1.18    fun merge _ _ : T = ref [];
    1.19  );
    1.20 @@ -1613,7 +1614,7 @@
    1.21            val (finished, unfinished) = List.partition Future.is_finished (! futures);
    1.22            val _ = futures := unfinished;
    1.23          in finished end)
    1.24 -      |> Future.join_results |> Exn.release_all |> null);
    1.25 +      |> Future.join_results |> null);
    1.26    in while not (joined ()) do () end;
    1.27  
    1.28  
    1.29 @@ -1667,6 +1668,7 @@
    1.30    in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
    1.31  
    1.32  val proof_of = Proofterm.proof_of o proof_body_of;
    1.33 +val force_proof = ignore o proof_body_of;
    1.34  
    1.35  
    1.36  (* closed derivations with official name *)