--- 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 ****)