# HG changeset patch
# User wenzelm
# Date 1570652537 -7200
# Node ID 83b7d1927fda0ce900cbf3ff7f6549d110581c52
# Parent  3ae7949ef05903c78682e27d5cd0cc01a6c10578
tuned;

diff -r 3ae7949ef059 -r 83b7d1927fda src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Wed Oct 09 22:18:23 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Wed Oct 09 22:22:17 2019 +0200
@@ -182,12 +182,13 @@
     val thy = Thm.theory_of_thm thm;
     val prop = Thm.full_prop_of thm;
     val prf = Thm.proof_of thm;
-    val prf' =
-      (case fst (Proofterm.strip_combt (fst (Proofterm.strip_combP prf))) of
-        PThm ({prop = prop', ...}, thm_body) =>
-          if prop = prop' then Proofterm.thm_body_proof_raw thm_body else prf
-      | _ => prf)
-  in if full then Proofterm.reconstruct_proof thy prop prf' else prf' end;
+  in
+    (case fst (Proofterm.strip_combt (fst (Proofterm.strip_combP prf))) of
+      PThm ({prop = prop', ...}, thm_body) =>
+        if prop = prop' then Proofterm.thm_body_proof_raw thm_body else prf
+    | _ => prf)
+    |> full ? Proofterm.reconstruct_proof thy prop
+  end;
 
 fun pretty_proof ctxt prf =
   Proof_Context.pretty_term_abbrev