# HG changeset patch
# User wenzelm
# Date 1703967751 -3600
# Node ID 0fb52d6ecb1be3e7bdeaea376eb43e2e79419357
# Parent  27e1cd1bba7630092c6b76c51b4969993b95e724
tuned;

diff -r 27e1cd1bba76 -r 0fb52d6ecb1b src/Pure/logic.ML
--- 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 =