--- a/src/Pure/Proof/reconstruct.ML Sat Feb 04 20:12:27 2017 +0100
+++ b/src/Pure/Proof/reconstruct.ML Sat Feb 04 21:15:11 2017 +0100
@@ -13,6 +13,7 @@
val proof_of : Proof.context -> thm -> Proofterm.proof
val expand_proof : Proof.context -> (string * term option) list ->
Proofterm.proof -> Proofterm.proof
+ val clean_proof_of : Proof.context -> bool -> thm -> Proofterm.proof
end;
structure Reconstruct : RECONSTRUCT =
@@ -388,4 +389,21 @@
in #3 (expand (Proofterm.maxidx_proof prf ~1) [] prf) end;
+
+(* cleanup for output etc. *)
+
+fun clean_proof_of ctxt full thm =
+ let
+ val (_, prop) =
+ Logic.unconstrainT (Thm.shyps_of thm)
+ (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
+ in
+ Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm))
+ |> reconstruct_proof ctxt prop
+ |> expand_proof ctxt [("", NONE)]
+ |> Proofterm.rew_proof (Proof_Context.theory_of ctxt)
+ |> Proofterm.no_thm_proofs
+ |> not full ? Proofterm.shrink_proof
+ end;
+
end;