src/Pure/logic.ML

--- a/src/Pure/logic.ML	Fri Dec 29 19:05:10 2023 +0100
+++ b/src/Pure/logic.ML	Fri Dec 29 19:22:15 2023 +0100
@@ -365,16 +365,18 @@
 
 fun unconstrainT shyps prop =
   let
-    val present = rev ((fold_types o fold_atyps_sorts) (insert (eq_fst op =)) prop []);
-    val extra = fold (Sorts.remove_sort o #2) present shyps;
+    val present = Types.build (prop |> (fold_types o fold_atyps) Types.add_set);
+    val present_sorts = map (fn T => (T, Term.dest_atyp_sort T)) (Types.list_set present);
 
-    val n = length present;
+    val extra = fold (Sorts.remove_sort o #2) present_sorts shyps;
+
+    val n = Types.size present;
     val (names1, names2) = Name.invent Name.context Name.aT (n + length extra) |> chop n;
 
     val present_map =
-      map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present names1;
+      map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present_sorts names1;
     val constraints_map =
-      map2 (fn (_, S) => fn a => (S, TVar ((a, 0), S))) present names1 @
+      map2 (fn (_, S) => fn a => (S, TVar ((a, 0), S))) present_sorts names1 @
       map2 (fn S => fn a => (S, TVar ((a, 0), S))) extra names2;
 
     fun atyp_map T =
@@ -392,7 +394,7 @@
         map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S);
 
     val outer_constraints =
-      maps (fn (T, S) => map (pair T) S) (present @ map (`dummy_tfree) extra);
+      maps (fn (T, S) => map (pair T) S) (present_sorts @ map (`dummy_tfree) extra);
 
     val ucontext =
      {present_map = present_map,