src/Pure/logic.ML

--- a/src/Pure/logic.ML	Tue Apr 18 12:10:00 2023 +0200
+++ b/src/Pure/logic.ML	Tue Apr 18 12:23:37 2023 +0200
@@ -66,7 +66,7 @@
     map_atyps: typ -> typ,
     constraints: ((typ * class) * term) list,
     outer_constraints: (typ * class) list};
-  val unconstrainT: Sortset.T -> term -> unconstrain_context * term
+  val unconstrainT: sort list -> term -> unconstrain_context * term
   val protectC: term
   val protect: term -> term
   val unprotect: term -> term
@@ -365,7 +365,7 @@
 fun unconstrainT shyps prop =
   let
     val present = rev ((fold_types o fold_atyps_sorts) (insert (eq_fst op =)) prop []);
-    val extra = Sortset.dest (fold (Sortset.remove o #2) present shyps);
+    val extra = fold (Sorts.remove_sort o #2) present shyps;
 
     val n = length present;
     val (names1, names2) = Name.invent Name.context Name.aT (n + length extra) |> chop n;