clarified signature: prefer Same.operation;

--- a/src/Pure/Proof/extraction.ML	Sat Dec 30 15:59:11 2023 +0100
+++ b/src/Pure/Proof/extraction.ML	Sat Dec 30 17:19:31 2023 +0100
@@ -389,8 +389,11 @@
       (build_rev (Term.add_vars prop'));
     val cs = maps (fn T => map (pair T) S) Ts;
     val constraints' = map Logic.mk_of_class cs;
-    fun typ_map T = Type.strip_sorts
-      (map_atyps (fn U => if member (op =) atyps U then #atyp_map ucontext U else U) T);
+    val typ_map = Type.strip_sorts o
+      Same.commit (Term_Subst.map_atypsT_same (fn U =>
+        if member (op =) atyps U
+        then #unconstrain_typ 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
   in

--- a/src/Pure/logic.ML	Sat Dec 30 15:59:11 2023 +0100
+++ b/src/Pure/logic.ML	Sat Dec 30 17:19:31 2023 +0100
@@ -60,10 +60,9 @@
   val dest_arity: term -> string * sort list * class
   val dummy_tfree: sort -> typ
   type unconstrain_context =
-   {atyp_map: typ -> typ,
-    map_atyps: typ -> typ,
+   {unconstrain_typ: {strip_sorts: bool} -> typ Same.operation,
     constraints: ((typ * class) * term) list,
-    outer_constraints: (typ * class) list};
+    outer_constraints: (typ * class) list}
   val unconstrainT: sort list -> term -> unconstrain_context * term
   val protectC: term
   val protect: term -> term
@@ -354,8 +353,7 @@
 fun dummy_tfree S = TFree ("'dummy", S);
 
 type unconstrain_context =
- {atyp_map: typ -> typ,
-  map_atyps: typ -> typ,
+ {unconstrain_typ: {strip_sorts: bool} -> typ Same.operation,
   constraints: ((typ * class) * term) list,
   outer_constraints: (typ * class) list};
 
@@ -374,15 +372,18 @@
       map2 (fn (_, S) => fn a => (S, TVar ((a, 0), S))) present names1 @
       map2 (fn S => fn a => (S, TVar ((a, 0), S))) extra names2;
 
-    fun atyp_map T =
+    fun unconstrain_atyp {strip_sorts} T =
       (case AList.lookup (op =) present_map T of
-        SOME U => U
+        SOME U => U |> strip_sorts ? Type.strip_sorts
       | NONE =>
           (case AList.lookup (op =) constraints_map (Type.sort_of_atyp T) of
-            SOME U => U
+            SOME U => U |> strip_sorts ? Type.strip_sorts
           | NONE => raise TYPE ("Dangling type variable ", [T], [prop])));
 
-    val map_atyps = Term.map_atyps (Type.strip_sorts o atyp_map);
+    fun unconstrain_typ strip_sorts =
+      Term_Subst.map_atypsT_same (fn T =>
+        let val T' = unconstrain_atyp strip_sorts T
+        in if T = T' then raise Same.SAME else T' end);
 
     val constraints =
       constraints_map |> maps (fn (_, T as TVar (ai, S)) =>
@@ -392,12 +393,11 @@
       maps (fn (T, S) => map (pair T) S) (present @ map (`dummy_tfree) extra);
 
     val ucontext =
-     {atyp_map = atyp_map,
-      map_atyps = map_atyps,
+     {unconstrain_typ = unconstrain_typ,
       constraints = constraints,
       outer_constraints = outer_constraints};
     val prop' = prop
-      |> Term.map_types map_atyps
+      |> Same.commit (Term_Subst.map_types_same (unconstrain_typ {strip_sorts = true}))
       |> curry list_implies (map #2 constraints);
   in (ucontext, prop') end;
 

--- a/src/Pure/proofterm.ML	Sat Dec 30 15:59:11 2023 +0100
+++ b/src/Pure/proofterm.ML	Sat Dec 30 17:19:31 2023 +0100
@@ -2139,9 +2139,11 @@
         SOME t => Hyp t
       | NONE => raise Fail "unconstrainT_proof: missing constraint");
 
-    val typ = Term_Subst.map_atypsT_same (Type.strip_sorts o #atyp_map ucontext);
+    val typ = #unconstrain_typ ucontext {strip_sorts = true};
+    val typ_sort = #unconstrain_typ ucontext {strip_sorts = false};
+
     fun ofclass (ty, c) =
-      let val ty' = Term.map_atyps (#atyp_map ucontext) ty;
+      let val ty' = Same.commit typ_sort ty;
       in the_single (of_sort_proof algebra classrel_proof arity_proof hyp_map (ty', [c])) end;
   in
     Same.commit (map_proof_same (Term_Subst.map_types_same typ) typ ofclass)
@@ -2182,7 +2184,7 @@
     val prop = Logic.list_implies (hyps, concl);
     val args = prop_args prop;
 
-    val (ucontext, prop1) = Logic.unconstrainT shyps prop;
+    val (ucontext as {unconstrain_typ, ...}, prop1) = Logic.unconstrainT shyps prop;
 
     val proofs = get_proofs_level ();
     val (zboxes1, zproof1) =
@@ -2241,7 +2243,9 @@
     val head = PThm (header, Thm_Body {open_proof = open_proof, body = thm_body});
     val proof2 =
       if unconstrain then
-        proof_combt' (head, (map o Option.map o Term.map_types) (#map_atyps ucontext) args)
+        proof_combt' (head,
+          (Same.commit o Same.map o Same.map_option o Term_Subst.map_types_same)
+            (unconstrain_typ {strip_sorts = true}) args)
       else
         proof_combP (proof_combt' (head, args),
           map PClass (#outer_constraints ucontext) @ map Hyp hyps);