diff -r 4c719b31a0c2 -r 5c1451900bec src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Thu Jan 11 15:37:11 2024 +0100
+++ b/src/Pure/zterm.ML	Thu Jan 11 16:34:40 2024 +0100
@@ -857,7 +857,7 @@
       ZTVars.build ((fold_proof_types {hyps = true} o fold_tvars) ZTVars.add_set prf);
     val present_set =
       Types.build (Types.add_atyps concl #> fold Types.add_atyps hyps #>
-        fold (Types.add_set o typ_of_tvar) (ZTVars.list_set present_set_prf));
+        ZTVars.fold (Types.add_set o typ_of_tvar o #1) present_set_prf);
     val ucontext as {constraints, outer_constraints, ...} =
       Logic.unconstrain_context [] present_set;