misc tuning and clarification: prefer Same.operation;

--- a/src/Pure/Isar/proof_context.ML	Tue Jan 09 16:04:21 2024 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Jan 09 17:10:09 2024 +0100
@@ -495,7 +495,7 @@
 
 
 fun cert_typ_mode mode ctxt T =
-  Type.cert_typ mode (tsig_of ctxt) T
+  Same.commit (Type.cert_typ_same mode (tsig_of ctxt)) T
     handle TYPE (msg, _, _) => error msg;
 
 val cert_typ = cert_typ_mode Type.mode_default;

--- a/src/Pure/consts.ML	Tue Jan 09 16:04:21 2024 +0100
+++ b/src/Pure/consts.ML	Tue Jan 09 17:10:09 2024 +0100
@@ -169,7 +169,7 @@
     fun err msg (c, T) =
       raise TYPE (msg ^ " " ^ quote c ^ " :: " ^
         Syntax.string_of_typ (Syntax.init_pretty context) T, [], []);
-    val certT = Type.cert_typ Type.mode_default tsig;
+    val certT = Same.commit (Type.cert_typ_same Type.mode_default tsig);
     fun cert tm =
       let
         val (head, args) = Term.strip_comb tm;
@@ -301,7 +301,7 @@
       error ("Illegal schematic variables on rhs of abbreviation " ^ Binding.print b);
 
     val rhs = raw_rhs
-      |> Term.map_types (Type.cert_typ Type.mode_default tsig)
+      |> Term.map_types (Type.cert_typ_same Type.mode_default tsig)
       |> cert_term
       |> Term.close_schematic_term;
     val normal_rhs = expand_term rhs;

--- a/src/Pure/sign.ML	Tue Jan 09 16:04:21 2024 +0100
+++ b/src/Pure/sign.ML	Tue Jan 09 17:10:09 2024 +0100
@@ -260,8 +260,8 @@
 
 val certify_class = Type.cert_class o tsig_of;
 val certify_sort = Type.cert_sort o tsig_of;
-val certify_typ = Type.cert_typ Type.mode_default o tsig_of;
-fun certify_typ_mode mode = Type.cert_typ mode o tsig_of;
+fun certify_typ_mode mode thy = Same.commit (Type.cert_typ_same mode (tsig_of thy));
+val certify_typ = certify_typ_mode Type.mode_default;
 
 
 (* certify term/prop *)

--- a/src/Pure/type.ML	Tue Jan 09 16:04:21 2024 +0100
+++ b/src/Pure/type.ML	Tue Jan 09 17:10:09 2024 +0100
@@ -53,7 +53,7 @@
   val check_decl: Context.generic -> tsig ->
     xstring * Position.T -> (string * Position.report list) * decl
   val the_decl: tsig -> string * Position.T -> decl
-  val cert_typ: mode -> tsig -> typ -> typ
+  val cert_typ_same: mode -> tsig -> typ Same.operation
   val arity_number: tsig -> string -> int
   val arity_sorts: Context.generic -> tsig -> string -> sort -> sort list
 
@@ -155,6 +155,10 @@
   Abbreviation of string list * typ * bool |
   Nonterminal;
 
+fun decl_args (LogicalType n) = n
+  | decl_args (Abbreviation (vs, _, _)) = length vs
+  | decl_args Nonterminal = 0;
+
 
 (* type tsig *)
 
@@ -265,42 +269,35 @@
 
 local
 
-fun inst_typ env (Type (c, Ts)) = Type (c, map (inst_typ env) Ts)
-  | inst_typ env (T as TFree (x, _)) = the_default T (AList.lookup (op =) env x)
-  | inst_typ _ T = T;
+fun inst_typ vs Ts =
+  Term_Subst.instantiateT_frees
+    (TFrees.build (fold2 (fn v => fn T => TFrees.add ((v, []), T)) vs Ts));
 
 in
 
-fun cert_typ (Mode {normalize, logical}) tsig ty =
+fun cert_typ_same (Mode {normalize, logical}) tsig =
   let
-    fun err msg = raise TYPE (msg, [ty], []);
-
-    val check_logical =
-      if logical then fn c => err ("Illegal occurrence of syntactic type: " ^ quote c)
-      else fn _ => ();
+    fun err T msg = raise TYPE (msg, [T], []);
+    fun err_syntactic T c = err T ("Illegal occurrence of syntactic type: " ^ quote c);
 
-    fun cert (T as Type (c, Ts)) =
-          let
-            val Ts' = map cert Ts;
-            fun nargs n = if length Ts <> n then err (bad_nargs c) else ();
-          in
-            (case the_decl tsig (c, Position.none) of
-              LogicalType n => (nargs n; Type (c, Ts'))
-            | Abbreviation (vs, U, syn) =>
-               (nargs (length vs);
-                if syn then check_logical c else ();
-                if normalize then inst_typ (vs ~~ Ts') U
-                else Type (c, Ts'))
-            | Nonterminal => (nargs 0; check_logical c; T))
+    fun sort S = (cert_sort tsig S; raise Same.SAME);
+    fun typ (T as Type (c, args)) =
+          let val decl = the_decl tsig (c, Position.none) in
+            if length args <> decl_args decl then err T (bad_nargs c)
+            else
+              (case decl of
+                LogicalType _ => Type (c, Same.map typ args)
+              | Abbreviation (vs, U, syntactic) =>
+                  if syntactic andalso logical then err_syntactic T c
+                  else if normalize then inst_typ vs (Same.commit (Same.map typ) args) U
+                  else Type (c, Same.map typ args)
+              | Nonterminal => if logical then err_syntactic T c else raise Same.SAME)
           end
-      | cert (TFree (x, S)) = TFree (x, cert_sort tsig S)
-      | cert (TVar (xi as (_, i), S)) =
-          if i < 0 then
-            err ("Malformed type variable: " ^ quote (Term.string_of_vname xi))
-          else TVar (xi, cert_sort tsig S);
-
-    val ty' = cert ty;
-  in if ty = ty' then ty else ty' end;  (*avoid copying of already normal type*)
+      | typ (TFree (_, S)) = sort S
+      | typ (T as TVar ((x, i), S)) =
+          if i < 0 then err T ("Malformed type variable: " ^ quote (Term.string_of_vname (x, i)))
+          else sort S;
+  in typ end;
 
 end;
 
@@ -691,7 +688,7 @@
   let
     fun err msg =
       cat_error msg ("The error(s) above occurred in type abbreviation " ^ Binding.print a);
-    val rhs' = Term.strip_sortsT (no_tvars (cert_typ mode_syntax tsig rhs))
+    val rhs' = Term.strip_sortsT (no_tvars (Same.commit (cert_typ_same mode_syntax tsig) rhs))
       handle TYPE (msg, _, _) => err msg;
     val _ =
       (case duplicates (op =) vs of