# HG changeset patch
# User wenzelm
# Date 1703970355 -3600
# Node ID 0596c28860f906bc8e31830c7bdf498181871b12
# Parent  d08460213400abf3ddbb00b5fc3e8d74fd96a469
clarified signature;

diff -r d08460213400 -r 0596c28860f9 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Sat Dec 30 21:54:08 2023 +0100
+++ b/src/Pure/logic.ML	Sat Dec 30 22:05:55 2023 +0100
@@ -58,6 +58,8 @@
   val mk_arities: arity -> term list
   val mk_arity: string * sort list * class -> term
   val dest_arity: term -> string * sort list * class
+  val present_sorts: sort Ord_List.T -> Types.set ->
+    {present: (typ * sort) list, extra: sort Ord_List.T}
   val dummy_tfree: sort -> typ
   type unconstrain_context =
    {unconstrain_typ: {strip_sorts: bool} -> typ Same.operation,
@@ -352,6 +354,12 @@
 
 fun dummy_tfree S = TFree ("'dummy", S);
 
+fun present_sorts shyps present_set =
+  let
+    val present = map (fn T => (T, Type.sort_of_atyp T)) (Types.list_set present_set);
+    val extra = fold (Sorts.remove_sort o #2) present shyps;
+  in {present = present, extra = extra} end;
+
 type unconstrain_context =
  {unconstrain_typ: {strip_sorts: bool} -> typ Same.operation,
   constraints: ((typ * class) * term) list,
@@ -360,8 +368,7 @@
 fun unconstrainT shyps prop =
   let
     val present_set = Types.build (prop |> (fold_types o fold_atyps) Types.add_set);
-    val present = map (fn T => (T, Type.sort_of_atyp T)) (Types.list_set present_set);
-    val extra = fold (Sorts.remove_sort o #2) present shyps;
+    val {present, extra} = present_sorts shyps present_set;
 
     val n = Types.size present_set;
     val (names1, names2) = Name.invent Name.context Name.aT (n + length extra) |> chop n;
diff -r d08460213400 -r 0596c28860f9 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Dec 30 21:54:08 2023 +0100
+++ b/src/Pure/thm.ML	Sat Dec 30 22:05:55 2023 +0100
@@ -1065,9 +1065,8 @@
 
         val present_set =
           Types.build (thm |> (fold_terms {hyps = true} o fold_types o fold_atyps) Types.add_set);
-        val present = map (fn T => (T, Type.sort_of_atyp T)) (Types.list_set present_set);
-
-        val extra = fold (Sorts.remove_sort o #2) present shyps;
+        val {present, extra} = Logic.present_sorts shyps present_set;
+
         val (witnessed, non_witnessed) =
           Sign.witness_sorts thy present extra ||> map (`(Sorts.minimize_sort algebra));