--- a/src/Pure/thm.ML Sun Jul 14 18:10:06 2024 +0200
+++ b/src/Pure/thm.ML Mon Jul 15 12:26:15 2024 +0200
@@ -1100,8 +1100,8 @@
SOME T' => T'
| NONE => raise Fail "strip_shyps: bad type variable in proof term"));
val map_ztyp =
- ZTypes.unsynchronized_cache
- (ZTerm.subst_type_same (ZTerm.ztyp_of o map_atyp o ZTerm.typ_of o ZTVar));
+ #apply (ZTypes.unsynchronized_cache
+ (ZTerm.subst_type_same (ZTerm.ztyp_of o map_atyp o ZTerm.typ_of o ZTVar)));
val zproof' = ZTerm.map_proof_types {hyps = true} map_ztyp zproof;
val proof' = Proofterm.map_proof_types (Term.map_atyps_same map_atyp) proof;