minor performance tuning: proper Same.operation;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Sun Dec 31 22:04:41 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Sun Dec 31 22:39:40 2023 +0100
@@ -99,7 +99,7 @@
       t' |> map_types
               (map_type_tvar
                 (fn (idxn, sort) =>
-                  if tvar_name_trivial idxn then dummyT else TVar (idxn, sort)))
+                  if tvar_name_trivial idxn then dummyT else raise Same.SAME))
 
     val subst =
       subst |> fold Vartab.delete trivial_tvar_names
@@ -107,7 +107,7 @@
                (K (apsnd (map_type_tfree
                            (fn (name, sort) =>
                               if tfree_name_trivial name then dummyT
-                              else TFree (name, sort)))))
+                              else raise Same.SAME))))
   in
     (t', subst)
   end

--- a/src/HOL/Tools/choice_specification.ML	Sun Dec 31 22:04:41 2023 +0100
+++ b/src/HOL/Tools/choice_specification.ML	Sun Dec 31 22:39:40 2023 +0100
@@ -60,7 +60,7 @@
     val fmap' = map Library.swap fmap
     fun unthaw v =
       (case AList.lookup (op =) fmap' v of
-        NONE => TVar v
+        NONE => raise Same.SAME
       | SOME w => TFree w)
   in map_types (map_type_tvar unthaw) t end
 

--- a/src/HOL/Types_To_Sets/unoverload_type.ML	Sun Dec 31 22:04:41 2023 +0100
+++ b/src/HOL/Types_To_Sets/unoverload_type.ML	Sun Dec 31 22:39:40 2023 +0100
@@ -20,7 +20,7 @@
 
 fun params_of_sort thy sort = maps (params_of_super_classes thy) sort
 
-fun subst_TFree n' ty' ty = map_type_tfree (fn x as (n, _) => if n = n' then ty' else TFree x) ty
+fun subst_TFree n' ty' ty = map_type_tfree (fn (n, _) => if n = n' then ty' else raise Same.SAME) ty
 
 fun unoverload_single_type context tvar thm =
   let

--- a/src/Pure/drule.ML	Sun Dec 31 22:04:41 2023 +0100
+++ b/src/Pure/drule.ML	Sun Dec 31 22:39:40 2023 +0100
@@ -759,10 +759,10 @@
                 in
                   raise THM ("infer_instantiate_types: type " ^
                     Syntax.string_of_typ ctxt (Envir.norm_type tyenv T) ^ " of variable " ^
-                    Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) t) ^
+                    Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type_same tyenv) t) ^
                     "\ncannot be unified with type " ^
                     Syntax.string_of_typ ctxt (Envir.norm_type tyenv U) ^ " of term " ^
-                    Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) u),
+                    Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type_same tyenv) u),
                     0, [th])
                 end;
           in (tyenv', maxidx'') end;

--- a/src/Pure/proofterm.ML	Sun Dec 31 22:04:41 2023 +0100
+++ b/src/Pure/proofterm.ML	Sun Dec 31 22:39:40 2023 +0100
@@ -828,7 +828,7 @@
 fun thawT names =
   map_type_tfree (fn (a, S) =>
     (case AList.lookup (op =) names a of
-      NONE => TFree (a, S)
+      NONE => raise Same.SAME
     | SOME ixn => TVar (ixn, S)));
 
 fun freeze names names' (t $ u) =
@@ -940,7 +940,7 @@
   (case Type.legacy_freezeT t of
     NONE => prf
   | SOME f =>
-      let val frzT = map_type_tvar (fn v => (case f v of NONE => TVar v | SOME T => T))
+      let val frzT = map_type_tvar (Same.function f)
       in map_proof_terms (map_types frzT) frzT prf end);
 
 

--- a/src/Pure/type.ML	Sun Dec 31 22:04:41 2023 +0100
+++ b/src/Pure/type.ML	Sun Dec 31 22:39:40 2023 +0100
@@ -361,7 +361,7 @@
     val tab = TFrees.make names;
     fun get v =
       (case TFrees.lookup tab v of
-        NONE => TFree v
+        NONE => raise Same.SAME
       | SOME w => TVar w);
   in (names, (map_types o map_type_tfree) get t) end;
 
@@ -402,7 +402,7 @@
       raise TYPE ("Failure during freezing of ?" ^ string_of_indexname ix, [], []);
 
 fun thaw_one alist (a, sort) = TVar (the (AList.lookup (op =) alist a), sort)
-  handle Option.Option => TFree (a, sort);
+  handle Option.Option => raise Same.SAME;
 
 in