# HG changeset patch
# User wenzelm
# Date 1704116168 -3600
# Node ID 9495bd0112d7b8d36b1cb06f8bccc4f0472d91cb
# Parent  1c758cd8d5b2f7c509e1ae8249a17d02adb2dcbc
clarified signature;

diff -r 1c758cd8d5b2 -r 9495bd0112d7 src/HOL/Types_To_Sets/internalize_sort.ML
--- a/src/HOL/Types_To_Sets/internalize_sort.ML	Sun Dec 31 22:39:40 2023 +0100
+++ b/src/HOL/Types_To_Sets/internalize_sort.ML	Mon Jan 01 14:36:08 2024 +0100
@@ -31,7 +31,8 @@
     val thy = Thm.theory_of_thm thm;
     val tvar = Thm.typ_of ctvar;
 
-    val ({constraints, outer_constraints, ...}, _) = Logic.unconstrainT [] (Thm.prop_of thm);
+    val {constraints, outer_constraints, ...} =
+      Logic.unconstrain_context [] (Types.build (Thm.prop_of thm |> Types.add_atyps));
 
     fun is_proper_class thy = can (Axclass.get_info thy); (* trick by FH *)
     fun reduce_to_non_proper_sort (TVar (name, sort)) =
diff -r 1c758cd8d5b2 -r 9495bd0112d7 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Sun Dec 31 22:39:40 2023 +0100
+++ b/src/Pure/logic.ML	Mon Jan 01 14:36:08 2024 +0100
@@ -65,7 +65,8 @@
    {typ_operation: {strip_sorts: bool} -> typ Same.operation,
     constraints: ((typ * class) * term) list,
     outer_constraints: (typ * class) list}
-  val unconstrainT: sort list -> term -> unconstrain_context * term
+  val unconstrain_context: sort Ord_List.T -> Types.set -> unconstrain_context
+  val unconstrainT: sort Ord_List.T -> term -> unconstrain_context * term
   val protectC: term
   val protect: term -> term
   val unprotect: term -> term
@@ -365,9 +366,8 @@
   constraints: ((typ * class) * term) list,
   outer_constraints: (typ * class) list};
 
-fun unconstrainT shyps prop =
+fun unconstrain_context shyps present_set =
   let
-    val present_set = Types.build (prop |> (fold_types o fold_atyps) Types.add_set);
     val {present, extra} = present_sorts shyps present_set;
 
     val n = Types.size present_set;
@@ -386,7 +386,7 @@
         | NONE =>
             (case AList.lookup (op =) constraints_map (Type.sort_of_atyp T) of
               SOME T' => T' |> strip_sorts ? Term.strip_sortsT
-            | NONE => raise TYPE ("Dangling type variable ", [T], [prop]))));
+            | NONE => raise TYPE ("Dangling type variable ", [T], []))));
 
     val typ_operation = Term.map_atyps_same o atyp_operation;
 
@@ -396,14 +396,18 @@
 
     val outer_constraints =
       maps (fn (T, S) => map (pair T) S) (present @ map (`dummy_tfree) extra);
+  in
+   {typ_operation = typ_operation,
+    constraints = constraints,
+    outer_constraints = outer_constraints}
+  end;
 
-    val ucontext =
-     {typ_operation = typ_operation,
-      constraints = constraints,
-      outer_constraints = outer_constraints};
+fun unconstrainT shyps prop =
+  let
+    val ucontext = unconstrain_context shyps (Types.build (prop |> Types.add_atyps));
     val prop' = prop
-      |> Term.map_types (typ_operation {strip_sorts = true})
-      |> curry list_implies (map #2 constraints);
+      |> Term.map_types (#typ_operation ucontext {strip_sorts = true})
+      |> curry list_implies (map #2 (#constraints ucontext));
   in (ucontext, prop') end;
 
 
diff -r 1c758cd8d5b2 -r 9495bd0112d7 src/Pure/term_items.ML
--- a/src/Pure/term_items.ML	Sun Dec 31 22:39:40 2023 +0100
+++ b/src/Pure/term_items.ML	Mon Jan 01 14:36:08 2024 +0100
@@ -222,4 +222,16 @@
 end;
 
 
-structure Types = Term_Items(type key = typ val ord = Term_Ord.typ_ord);
+structure Types:
+sig
+  include TERM_ITEMS
+  val add_atyps: term -> set -> set
+end =
+struct
+
+structure Term_Items = Term_Items(type key = typ val ord = Term_Ord.typ_ord);
+open Term_Items;
+
+val add_atyps = (fold_types o fold_atyps) add_set;
+
+end;
diff -r 1c758cd8d5b2 -r 9495bd0112d7 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Dec 31 22:39:40 2023 +0100
+++ b/src/Pure/thm.ML	Mon Jan 01 14:36:08 2024 +0100
@@ -1065,8 +1065,7 @@
         fun lt (S1, S2) = le (S1, S2) andalso not (le (S2, S1));
         fun rel (S1, S2) = if S1 = S2 then [] else [(Term.aT S1, S2)];
 
-        val present_set =
-          Types.build (thm |> (fold_terms {hyps = true} o fold_types o fold_atyps) Types.add_set);
+        val present_set = Types.build (thm |> fold_terms {hyps = true} Types.add_atyps);
         val {present, extra} = Logic.present_sorts shyps present_set;
 
         val (witnessed, non_witnessed) =