tuned;

--- a/src/Pure/logic.ML	Sat Dec 30 21:22:11 2023 +0100
+++ b/src/Pure/logic.ML	Sat Dec 30 21:22:31 2023 +0100
@@ -369,7 +369,7 @@
     val present_map =
       map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present names1;
     val constraints_map =
-      map2 (fn (_, S) => fn a => (S, TVar ((a, 0), S))) present names1 @
+      map (fn (_, V) => (Type.sort_of_atyp V, V)) present_map @
       map2 (fn S => fn a => (S, TVar ((a, 0), S))) extra names2;
 
     fun unconstrain_atyp {strip_sorts} T =