# HG changeset patch
# User wenzelm
# Date 1704745821 -3600
# Node ID 88341f610b3309e2f9091a9006574001fa3741a2
# Parent  af4f6b82719fee9235a0f33fd99ce2cc06debf11
minor performance tuning;

diff -r af4f6b82719f -r 88341f610b33 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Mon Jan 08 13:41:45 2024 +0100
+++ b/src/Pure/type_infer.ML	Mon Jan 08 21:30:21 2024 +0100
@@ -117,6 +117,6 @@
     val params = TVars.build (fold TVars.add_tvars ts) |> TVars.list_set;
     val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
     val (inst, _) = fold subst_param params (TVars.empty, used);
-  in (map o map_types) (Term_Subst.instantiateT inst) ts end;
+  in (Same.commit o Same.map o Term.map_types_same) (Term_Subst.instantiateT_same inst) ts end;
 
 end;
diff -r af4f6b82719f -r 88341f610b33 src/Pure/type_infer_context.ML
--- a/src/Pure/type_infer_context.ML	Mon Jan 08 13:41:45 2024 +0100
+++ b/src/Pure/type_infer_context.ML	Mon Jan 08 21:30:21 2024 +0100
@@ -288,7 +288,7 @@
     val constrain_vars = Term.map_aterms
       (fn Free (x, T) => Type.constraint T (Free (x, var_type ctxt (x, ~1)))
         | Var (xi, T) => Type.constraint T (Var (xi, var_type ctxt xi))
-        | t => t);
+        | _ => raise Same.SAME);
 
     val ts = burrow_types (Syntax.check_typs ctxt) raw_ts;
     val idx = Type_Infer.param_maxidx_of ts + 1;