src/Pure/Proof/reconstruct.ML

 sig
   val quiet_mode : bool Unsynchronized.ref
   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;
 
 structure Reconstruct : RECONSTRUCT =

   | prop_of0 _ _ = error "prop_of: partial proof object";
 
 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 ****)
 
 fun expand_proof thy thms prf =
   let