src/Pure/proofterm.ML

   val proof_combt: proof * term list -> proof
   val proof_combt': proof * term option list -> proof
   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
   val map_proof_types_same: typ Same.operation -> proof Same.operation
   val map_proof_terms: (term -> term) -> (typ -> typ) -> proof -> proof

 fun strip_combP prf =
     let fun stripc (prf %% prf', prfs) = stripc (prf, prf'::prfs)
           | 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);
 
 val mk_Abst = fold_rev (fn (x, _: typ) => fn prf => Abst (x, NONE, prf));