# HG changeset patch
# User wenzelm
# Date 1703947818 -3600
# Node ID 10925576fbb42a944e130285fae1395d7301ace2
# Parent  e6a12ea61f83d31446f84044eb1367f3c8592b65
more zproofs;

diff -r e6a12ea61f83 -r 10925576fbb4 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Dec 30 12:34:27 2023 +0100
+++ b/src/Pure/thm.ML	Sat Dec 30 15:50:18 2023 +0100
@@ -1095,11 +1095,14 @@
             (case get_replacement (Type.sort_of_atyp T) of
               SOME T' => T'
             | NONE => raise Fail "strip_shyps: bad type variable in proof term");
-
-        val proof' = proof
-          |> Same.commit (Proofterm.map_proof_types_same (Term_Subst.map_atypsT_same replace_atyp));
+        val replace_ztyp =
+          ZTypes.unsynchronized_cache
+            (ZTerm.subst_type_same (ZTerm.ztyp_of o replace_atyp o ZTerm.typ_of o ZTVar));
+
+        val zproof' = ZTerm.map_proof_types replace_ztyp zproof;
+        val proof' = Proofterm.map_proof_types (Term_Subst.map_atypsT_same replace_atyp) proof;
       in
-        Thm (make_deriv promises oracles thms zboxes zproof proof',
+        Thm (make_deriv promises oracles thms zboxes zproof' proof',
          {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints',
           shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
       end)