diff -r 5d367ceecf56 -r 656ff92bad48 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Mon Aug 08 19:59:35 2011 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Mon Aug 08 20:21:49 2011 +0200
@@ -10,6 +10,7 @@
   val reconstruct_proof : theory -> term -> Proofterm.proof -> Proofterm.proof
   val prop_of' : term list -> Proofterm.proof -> term
   val prop_of : Proofterm.proof -> term
+  val proof_of : thm -> Proofterm.proof
   val expand_proof : theory -> (string * term option) list ->
     Proofterm.proof -> Proofterm.proof
 end;
@@ -323,6 +324,10 @@
 val prop_of' = Envir.beta_eta_contract oo prop_of0;
 val prop_of = prop_of' [];
 
+fun proof_of thm =
+  reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
+
+
 
 (**** expand and reconstruct subproofs ****)