src/Pure/Proof/proof_syntax.ML

   let
     val thy = Thm.theory_of_thm thm;
     val prop = Thm.full_prop_of thm;
     val prf = Thm.proof_of thm;
     val prf' = (case strip_combt (fst (strip_combP prf)) of
-        (PThm (_, ((_, prop', _), body)), _) => if prop = prop' then force_proof body else prf
+        (PThm (_, ((_, prop', _), body)), _) => if prop = prop' then join_proof body else prf
       | _ => prf)
   in if full then Reconstruct.reconstruct_proof thy prop prf' else prf' end;
 
 fun pretty_proof ctxt prf =
   ProofContext.pretty_term_abbrev