--- a/src/Pure/proofterm.ML Fri Oct 11 11:16:36 2019 +0200
+++ b/src/Pure/proofterm.ML Fri Oct 11 15:36:32 2019 +0200
@@ -77,7 +77,8 @@
val proof_combP: proof * proof list -> proof
val strip_combt: proof -> proof * term option list
val strip_combP: proof -> proof * proof list
- val strip_thm: proof_body -> proof_body
+ val strip_thm_proof: proof -> proof
+ val strip_thm_body: proof_body -> proof_body
val map_proof_same: term Same.operation -> typ Same.operation
-> (typ * class -> proof) -> proof Same.operation
val map_proof_terms_same: term Same.operation -> typ Same.operation -> proof Same.operation
@@ -451,7 +452,12 @@
| stripc x = x
in stripc (prf, []) end;
-fun strip_thm (body as PBody {proof, ...}) =
+fun strip_thm_proof proof =
+ (case fst (strip_combt (fst (strip_combP proof))) of
+ PThm (_, thm_body) => thm_body_proof_raw thm_body
+ | _ => proof);
+
+fun strip_thm_body (body as PBody {proof, ...}) =
(case fst (strip_combt (fst (strip_combP proof))) of
PThm (_, Thm_Body {body = body', ...}) => Future.join body'
| _ => body);