more accurate treatment of term variables after instantiation of type variables;

--- a/src/Pure/term_items.ML	Wed Dec 06 13:04:07 2023 +0100
+++ b/src/Pure/term_items.ML	Wed Dec 06 13:16:34 2023 +0100
@@ -32,6 +32,7 @@
   val make1: key * 'a -> 'a table
   val make2: key * 'a -> key * 'a -> 'a table
   val make3: key * 'a -> key * 'a -> key * 'a -> 'a table
+  val make_strict: (key * 'a) list -> 'a table
   type set = int table
   val add_set: key -> set -> set
   val make_set: key list -> set
@@ -81,6 +82,8 @@
 fun make2 e1 e2 = build (add e1 #> add e2);
 fun make3 e1 e2 e3 = build (add e1 #> add e2 #> add e3);
 
+fun make_strict es = Table (Table.make es);
+
 
 (* set with order of addition *)
 

--- a/src/Pure/zterm.ML	Wed Dec 06 13:04:07 2023 +0100
+++ b/src/Pure/zterm.ML	Wed Dec 06 13:16:34 2023 +0100
@@ -236,21 +236,33 @@
 fun map_insts_same typ term (instT, inst) =
   let
     val changed = Unsynchronized.ref false;
+    fun apply f x =
+      (case Same.catch f x of
+        NONE => NONE
+      | some => (changed := true; some));
+
     val instT' =
       (instT, instT) |-> ZTVars.fold (fn (v, T) =>
-        (case Same.catch typ T of
-          SOME U => (changed := true; ZTVars.update (v, U))
-        | NONE => I));
+        (case apply typ T of
+          NONE => I
+        | SOME T' => ZTVars.update (v, T')));
+
+    val vars' =
+      (inst, ZVars.empty) |-> ZVars.fold (fn ((v, T), _) =>
+        (case apply typ T of
+          NONE => I
+        | SOME T' => ZVars.add ((v, T), (v, T'))));
+
     val inst' =
-      if ! changed then
+      if ZVars.is_empty vars' then
+        (inst, inst) |-> ZVars.fold (fn (v, t) =>
+          (case apply term t of
+            NONE => I
+          | SOME t' => ZVars.update (v, t')))
+      else
         ZVars.dest inst
-        |> map (fn ((x, T), t) => ((x, Same.commit typ T), Same.commit term t))
-        |> ZVars.make
-      else
-        (inst, inst) |-> ZVars.fold (fn (v, t) =>
-          (case Same.catch term t of
-            SOME u => (changed := true; ZVars.update (v, u))
-          | NONE => I));
+        |> map (fn (v, t) => (the_default v (ZVars.lookup vars' v), the_default t (apply term t)))
+        |> ZVars.make_strict;
   in if ! changed then (instT', inst') else raise Same.SAME end;
 
 fun map_proof_same typ term =