diff -r 27279c76a068 -r e1b2595d678a src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Wed Jan 10 22:25:34 2024 +0100
+++ b/src/Pure/zterm.ML	Thu Jan 11 12:00:02 2024 +0100
@@ -830,7 +830,7 @@
   let
     val {zterm, ...} = zterm_cache thy;
 
-    val present_set = Types.build (fold Types.add_atyps hyps #> Types.add_atyps concl);
+    val present_set = Types.build (Types.add_atyps concl #> fold Types.add_atyps hyps);
     val ucontext as {constraints, outer_constraints, ...} =
       Logic.unconstrain_context [] present_set;