--- a/src/Pure/thm.ML Sun Dec 31 18:49:00 2023 +0100
+++ b/src/Pure/thm.ML Sun Dec 31 19:24:37 2023 +0100
@@ -1102,7 +1102,7 @@
(ZTerm.subst_type_same (ZTerm.ztyp_of o map_atyp o ZTerm.typ_of o ZTVar));
val zproof' = ZTerm.map_proof_types map_ztyp zproof;
- val proof' = Proofterm.map_proof_types (Term_Subst.map_atypsT_same map_atyp) proof;
+ val proof' = Proofterm.map_proof_types (Term.map_atyps_same map_atyp) proof;
in
Thm (make_deriv promises oracles thms zboxes zproof' proof',
{cert = cert, tags = tags, maxidx = maxidx, constraints = constraints',