--- a/src/HOL/Tools/rewrite_hol_proof.ML Mon Jan 08 22:53:38 2024 +0100
+++ b/src/HOL/Tools/rewrite_hol_proof.ML Mon Jan 08 23:17:32 2024 +0100
@@ -310,8 +310,8 @@
| strip_cong ps (PThm ({name = "HOL.refl", ...}, _) % SOME f %% _) = SOME (f, ps)
| strip_cong _ _ = NONE;
-val subst_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of @{thm subst}))));
-val sym_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of@{thm sym}))));
+val subst_prf = Proofterm.any_head_of (Thm.proof_of @{thm subst});
+val sym_prf = Proofterm.any_head_of (Thm.proof_of @{thm sym});
fun make_subst Ts prf xs (_, []) = prf
| make_subst Ts prf xs (f, ((x, y), (prf', clprf)) :: ps) =