src/Pure/thm.ML

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

     val _ = Exn.release_all (map (Future.join_result o #2) (rev open_promises));
     val ps = map (apsnd (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;
+val join_proof = ignore o proof_body_of;
 
 
 (* closed derivations with official name *)
 
 fun get_name thm =