1.1 --- a/src/Pure/Proof/reconstruct.ML	Mon Aug 08 19:59:35 2011 +0200
     1.2 +++ b/src/Pure/Proof/reconstruct.ML	Mon Aug 08 20:21:49 2011 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4    val reconstruct_proof : theory -> term -> Proofterm.proof -> Proofterm.proof
     1.5    val prop_of' : term list -> Proofterm.proof -> term
     1.6    val prop_of : Proofterm.proof -> term
     1.7 +  val proof_of : thm -> Proofterm.proof
     1.8    val expand_proof : theory -> (string * term option) list ->
     1.9      Proofterm.proof -> Proofterm.proof
    1.10  end;
    1.11 @@ -323,6 +324,10 @@
    1.12  val prop_of' = Envir.beta_eta_contract oo prop_of0;
    1.13  val prop_of = prop_of' [];
    1.14  
    1.15 +fun proof_of thm =
    1.16 +  reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
    1.17 +
    1.18 +
    1.19  
    1.20  (**** expand and reconstruct subproofs ****)
    1.21