--- a/src/Pure/Proof/proof_syntax.ML Mon Jan 26 22:15:35 2009 +0100
+++ b/src/Pure/Proof/proof_syntax.ML Tue Jan 27 00:29:37 2009 +0100
@@ -228,7 +228,7 @@
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;