# HG changeset patch
# User wenzelm
# Date 1737659174 -3600
# Node ID 87cc86357dc2e7f1372222d406aa4a2115bfab24
# Parent  adda8961df7bb1ade02a6017cfc570629e7319a5
proper treatment of variables with the same name, but different sorts/types: this routinely happens in HOL Light (see also 0e2f019477e2), as well as theory "HOL-Algebra.Algebraic_Closure_Type" (line 77);

diff -r adda8961df7b -r 87cc86357dc2 src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Thu Jan 23 14:25:31 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Thu Jan 23 20:06:14 2025 +0100
@@ -170,7 +170,6 @@
         Frees.add (Term.dest_Free (Thm.term_of a), b)))
   in
     Thm.instantiate_frees (TFrees.empty, inst) th
-    |> freeze'
   end
 
 
diff -r adda8961df7b -r 87cc86357dc2 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu Jan 23 14:25:31 2025 +0100
+++ b/src/Pure/more_thm.ML	Thu Jan 23 20:06:14 2025 +0100
@@ -408,19 +408,43 @@
   if TFrees.is_empty instT andalso Frees.is_empty inst then th
   else
     let
-      val tfrees = Names.build (TFrees.fold (Names.add_set o #1 o #1) instT);
-      val frees = Names.build (Frees.fold (Names.add_set o #1 o #1) inst);
+      val namesT = Names.build (TFrees.fold (Names.add_set o #1 o #1) instT);
+      val names = Names.build (Frees.fold (Names.add_set o #1 o #1) inst);
+
+      val idx =
+        (Thm.maxidx_of th
+          |> TFrees.fold (Integer.max o Thm.maxidx_of_ctyp o #2) instT
+          |> Frees.fold (Integer.max o Thm.maxidx_of_cterm o #2) inst) + 1;
+      fun index ((a, A), b) = (((a, idx), A), b);
 
-      val idx = Thm.maxidx_of th + 1;
-      fun index ((a, A), b) = (((a, idx), A), b);
-      val instT' = TVars.build (TFrees.fold (TVars.add o index) instT);
-      val inst' = Vars.build (Frees.fold (Vars.add o index) inst);
+      val instT' =
+        TVars.build (TFrees.fold (TVars.add o index) instT)
+        |> not (Names.is_empty namesT) ? Thm.fold_atomic_ctyps {hyps = true}
+            (fn TFree (a, S) => Names.defined namesT a andalso not (TFrees.defined instT (a, S))
+              | _ => false)
+            (fn cT =>
+              let val (a, S) = dest_TFree (Thm.typ_of cT)
+              in TVars.add (((a, idx), S), cT) end) th;
+
+      val inst_typ = Term_Subst.instantiateT_frees (TFrees.map (K Thm.typ_of) instT);
+      val inst_ctyp =
+        Thm.generalize_cterm (namesT, Names.empty) idx #>
+        Thm.instantiate_cterm (instT', Vars.empty);
+
+      val inst' =
+        Vars.build (Frees.fold (Vars.add o index) inst)
+        |> not (Names.is_empty names) ? Thm.fold_atomic_cterms {hyps = true}
+            (fn Free (x, T) => Names.defined names x andalso not (Frees.defined inst (x, inst_typ T))
+              | _ => false)
+            (fn ct =>
+              let val (x, T) = dest_Free (Thm.term_of ct)
+              in Vars.add (((x, idx), inst_typ T), inst_ctyp ct) end) th;
 
       val hyps = Thm.chyps_of th;
     in
       th
       |> fold_rev Thm.implies_intr hyps
-      |> Thm.generalize (tfrees, frees) idx
+      |> Thm.generalize (namesT, names) idx
       |> Thm.instantiate (instT', inst')
       |> assume_prems (length hyps)
     end;
diff -r adda8961df7b -r 87cc86357dc2 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Jan 23 14:25:31 2025 +0100
+++ b/src/Pure/thm.ML	Thu Jan 23 20:06:14 2025 +0100
@@ -31,6 +31,7 @@
   val dest_ctyp: ctyp -> ctyp list
   val dest_ctypN: int -> ctyp -> ctyp
   val make_ctyp: ctyp -> ctyp list -> ctyp
+  val maxidx_of_ctyp: ctyp -> int
   (*certified terms*)
   val term_of: cterm -> term
   val typ_of_cterm: cterm -> typ
@@ -207,6 +208,8 @@
 
 fun typ_of (Ctyp {T, ...}) = T;
 
+fun maxidx_of_ctyp (Ctyp {maxidx, ...}) = maxidx;
+
 fun global_ctyp_of thy raw_T =
   let
     val T = Sign.certify_typ thy raw_T;