# HG changeset patch
# User wenzelm
# Date 1228518541 -3600
# Node ID d8d3cbbb6fcc17f9fdf1e82e5a9e9baa2e86110f
# Parent  c9cdb569487a4dc05eefbee36e4a6d965b772df8
renamed force_proof to join_proof;

diff -r c9cdb569487a -r d8d3cbbb6fcc src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Dec 06 00:08:32 2008 +0100
+++ b/src/Pure/thm.ML	Sat Dec 06 00:09:01 2008 +0100
@@ -149,7 +149,7 @@
   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;
@@ -1638,7 +1638,7 @@
   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 *)