diff -r 69592ac04836 -r b81a048960a3 src/Pure/Proof/reconstruct.ML
--- 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;