src/Pure/more_thm.ML

     val thy = Thm.theory_of_thm thm;
     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))
+    Proofterm.strip_thm_proof (Thm.proof_of thm)
     |> Proofterm.reconstruct_proof thy prop
     |> Proofterm.expand_proof thy [("", NONE)]
     |> Proofterm.rew_proof thy
     |> Proofterm.no_thm_proofs
     |> not full ? Proofterm.shrink_proof