# HG changeset patch
# User wenzelm
# Date 1704747260 -3600
# Node ID 032ca41f590a03d13873be4bdbd568c6d35d7778
# Parent  8480736373881b88349bec764292c4480d1a415e
minor performance tuning;

diff -r 848073637388 -r 032ca41f590a src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Mon Jan 08 21:53:27 2024 +0100
+++ b/src/Pure/Isar/class.ML	Mon Jan 08 21:54:20 2024 +0100
@@ -428,9 +428,11 @@
 fun canonical_abbrev class phi prmode with_syntax ((b, mx), rhs) thy =
   let
     val c = Sign.full_name thy b;
-    val constrain = map_atyps (fn T as TFree (v, _) =>
-      if v = Name.aT then TFree (v, [class]) else T | T => T);
-    val rhs' = map_types constrain rhs;
+    val constrain =
+      (Term.map_types o Term.map_atyps_same)
+        (fn TFree (a, _) => if a = Name.aT then TFree (a, [class]) else raise Same.SAME
+          | _ => raise Same.SAME);
+    val rhs' = constrain rhs;
   in
     thy
     |> Sign.add_abbrev (#1 prmode) (b, Logic.varify_types_global rhs')
@@ -614,9 +616,14 @@
       | matchings _ = I;
     val tvartab = Vartab.build ((fold o fold_aterms) matchings ts)
       handle Sorts.CLASS_ERROR e => error (Sorts.class_error (Context.Proof ctxt) e);
-    val inst = map_type_tvar
-      (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
-  in if Vartab.is_empty tvartab then ts else (map o map_types) inst ts end;
+    val inst_same =
+      (Same.map o Term.map_types_same o Term.map_atyps_same)
+        (fn TVar (vi, S) =>
+            (case Vartab.lookup tvartab vi of
+              SOME S' => if S = S' then raise Same.SAME else TVar (vi, S')
+            | NONE => raise Same.SAME)
+          | _ => raise Same.SAME);
+  in if Vartab.is_empty tvartab then ts else Same.commit inst_same ts end;
 
 
 (* target *)
diff -r 848073637388 -r 032ca41f590a src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Mon Jan 08 21:53:27 2024 +0100
+++ b/src/Pure/Isar/class_declaration.ML	Mon Jan 08 21:54:20 2024 +0100
@@ -99,7 +99,7 @@
       (case some_prop of
         NONE => of_class_prop_concl
       | SOME prop => Logic.mk_implies (Morphism.term const_morph
-          ((map_types o map_atyps) (K a_type) prop), of_class_prop_concl));
+          ((map_types o Term.map_atyps_same) (K a_type) prop), of_class_prop_concl));
     val sup_of_classes = map (snd o Class.rules thy) sups;
     val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class);
     val axclass_intro = #intro (Axclass.get_info thy class);
@@ -147,8 +147,9 @@
           | _ => error "Multiple type variables in class specification");
         val fixateT = Term.aT fixate_sort;
       in
-        (map o map_atyps)
-          (fn T as TVar (xi, _) => if Type_Infer.is_param xi then fixateT else T | T => T) Ts
+        (Same.commit o Same.map o Term.map_atyps_same)
+          (fn TVar (xi, _) => if Type_Infer.is_param xi then fixateT else raise Same.SAME
+            | _ => raise Same.SAME) Ts
       end);
     fun unify_params ts =
       let
@@ -302,7 +303,7 @@
     (*FIXME simplify*)
     fun globalize param_map = map_aterms
       (fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty)
-        | t => t);
+        | _ => raise Same.SAME);
     val raw_pred = Locale.intros_of thy class
       |> fst
       |> Option.map (Logic.unvarify_global o Logic.strip_imp_concl o Thm.prop_of);
diff -r 848073637388 -r 032ca41f590a src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Mon Jan 08 21:53:27 2024 +0100
+++ b/src/Pure/Isar/overloading.ML	Mon Jan 08 21:54:20 2024 +0100
@@ -79,7 +79,7 @@
     val improvements = Vartab.build ((fold o fold_aterms) accumulate_improvements ts);
     val ts' =
       ts
-      |> (map o map_types) (Envir.subst_type improvements)
+      |> (Same.commit o Same.map o Term.map_types_same) (Envir.subst_type_same improvements)
       |> not no_subst ? map apply_subst;
   in
     if secondary_pass orelse no_subst then
diff -r 848073637388 -r 032ca41f590a src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Mon Jan 08 21:53:27 2024 +0100
+++ b/src/Pure/axclass.ML	Mon Jan 08 21:54:20 2024 +0100
@@ -381,7 +381,7 @@
       | [] => ()
       | _ => error ("Multiple type variables in class axiom:\n" ^ Syntax.string_of_term ctxt t);
       t
-      |> Term.map_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U))
+      |> (Term.map_types o Term.map_atyps_same) (fn TFree _ => Term.aT [] | _ => raise Same.SAME)
       |> Logic.close_form);
 
     val axiomss = map (map (prep_axiom o Sign.cert_prop thy) o snd) raw_specs;