tuned signature;

--- a/src/Pure/Proof/extraction.ML	Sun Dec 31 15:16:05 2023 +0100
+++ b/src/Pure/Proof/extraction.ML	Sun Dec 31 16:15:27 2023 +0100
@@ -392,7 +392,7 @@
     val typ_map = Type.strip_sorts o
       Term_Subst.map_atypsT (fn U =>
         if member (op =) atyps U
-        then #unconstrain_typ ucontext {strip_sorts = false} U
+        then #typ_operation ucontext {strip_sorts = false} U
         else raise Same.SAME);
     fun mk_hyp (T, c) = Hyp (Logic.mk_of_class (typ_map T, c));
     val xs' = map (map_types typ_map) xs

--- a/src/Pure/logic.ML	Sun Dec 31 15:16:05 2023 +0100
+++ b/src/Pure/logic.ML	Sun Dec 31 16:15:27 2023 +0100
@@ -62,7 +62,7 @@
     {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,
+   {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
@@ -361,7 +361,7 @@
   in {present = present, extra = extra} end;
 
 type unconstrain_context =
- {unconstrain_typ: {strip_sorts: bool} -> typ Same.operation,
+ {typ_operation: {strip_sorts: bool} -> typ Same.operation,
   constraints: ((typ * class) * term) list,
   outer_constraints: (typ * class) list};
 
@@ -379,7 +379,7 @@
       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 =
+    fun atyp_operation {strip_sorts} T =
       (case AList.lookup (op =) present_map T of
         SOME U => U |> strip_sorts ? Type.strip_sorts
       | NONE =>
@@ -387,9 +387,9 @@
             SOME U => U |> strip_sorts ? Type.strip_sorts
           | NONE => raise TYPE ("Dangling type variable ", [T], [prop])));
 
-    fun unconstrain_typ strip_sorts =
+    fun typ_operation strip_sorts =
       Term_Subst.map_atypsT_same (fn T =>
-        let val T' = unconstrain_atyp strip_sorts T
+        let val T' = atyp_operation strip_sorts T
         in if T = T' then raise Same.SAME else T' end);
 
     val constraints =
@@ -400,11 +400,11 @@
       maps (fn (T, S) => map (pair T) S) (present @ map (`dummy_tfree) extra);
 
     val ucontext =
-     {unconstrain_typ = unconstrain_typ,
+     {typ_operation = typ_operation,
       constraints = constraints,
       outer_constraints = outer_constraints};
     val prop' = prop
-      |> Term_Subst.map_types (unconstrain_typ {strip_sorts = true})
+      |> Term_Subst.map_types (typ_operation {strip_sorts = true})
       |> curry list_implies (map #2 constraints);
   in (ucontext, prop') end;
 

--- a/src/Pure/proofterm.ML	Sun Dec 31 15:16:05 2023 +0100
+++ b/src/Pure/proofterm.ML	Sun Dec 31 16:15:27 2023 +0100
@@ -1106,8 +1106,8 @@
 
 fun unconstrainT_proof algebra sorts_proof (ucontext: Logic.unconstrain_context) =
   let
-    val typ = #unconstrain_typ ucontext {strip_sorts = true};
-    val typ_sort = #unconstrain_typ ucontext {strip_sorts = false};
+    val typ = #typ_operation ucontext {strip_sorts = true};
+    val typ_sort = #typ_operation ucontext {strip_sorts = false};
 
     fun hyps T =
       (case AList.lookup (op =) (#constraints ucontext) T of
@@ -2181,7 +2181,7 @@
     val prop = Logic.list_implies (hyps, concl);
     val args = prop_args prop;
 
-    val (ucontext as {unconstrain_typ, ...}, prop1) = Logic.unconstrainT shyps prop;
+    val (ucontext as {typ_operation, ...}, prop1) = Logic.unconstrainT shyps prop;
 
     val proofs = get_proofs_level ();
     val (zboxes1, zproof1) =
@@ -2241,7 +2241,7 @@
       if unconstrain then
         proof_combt' (head,
           (Same.commit o Same.map o Same.map_option o Term_Subst.map_types_same)
-            (unconstrain_typ {strip_sorts = true}) args)
+            (typ_operation {strip_sorts = true}) args)
       else
         proof_combP (proof_combt' (head, args),
           map PClass (#outer_constraints ucontext) @ map Hyp hyps);