tuned;
authorwenzelm
Wed, 09 Oct 2019 22:22:17 +0200
changeset 71003 83b7d1927fda
parent 71002 3ae7949ef059
child 71004 a6644dfe8e26
tuned;
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