1.1 --- a/src/Pure/thm.ML	Sat Dec 06 00:08:32 2008 +0100
     1.2 +++ b/src/Pure/thm.ML	Sat Dec 06 00:09:01 2008 +0100
     1.3 @@ -149,7 +149,7 @@
     1.4    val future: thm future -> 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 join_proof: thm -> unit
     1.9    val extern_oracles: theory -> xstring list
    1.10    val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
    1.11  end;
    1.12 @@ -1638,7 +1638,7 @@
    1.13    in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
    1.14  
    1.15  val proof_of = Proofterm.proof_of o proof_body_of;
    1.16 -val force_proof = ignore o proof_body_of;
    1.17 +val join_proof = ignore o proof_body_of;
    1.18  
    1.19  
    1.20  (* closed derivations with official name *)