--- a/src/Pure/thm.ML Fri Nov 08 16:25:18 2019 +0100
+++ b/src/Pure/thm.ML Fri Nov 08 19:06:50 2019 +0100
@@ -101,6 +101,7 @@
val proof_bodies_of: thm list -> proof_body list
val proof_body_of: thm -> proof_body
val proof_of: thm -> proof
+ val reconstruct_proof_of: thm -> Proofterm.proof
val consolidate: thm list -> unit
val expose_proofs: theory -> thm list -> unit
val expose_proof: theory -> thm -> unit
@@ -760,6 +761,9 @@
val proof_body_of = singleton proof_bodies_of;
val proof_of = Proofterm.proof_of o proof_body_of;
+fun reconstruct_proof_of thm =
+ Proofterm.reconstruct_proof (theory_of_thm thm) (prop_of thm) (proof_of thm);
+
val consolidate = ignore o proof_bodies_of;
fun expose_proofs thy thms =