misc tuning and clarification;
eliminate clones (see also 3ae09d27ee7a);

--- a/src/HOL/Tools/choice_specification.ML	Tue Dec 05 20:07:52 2023 +0100
+++ b/src/HOL/Tools/choice_specification.ML	Tue Dec 05 20:56:51 2023 +0100
@@ -57,10 +57,10 @@
 fun unvarify_global t fmap =
   let
     val fmap' = map Library.swap fmap
-    fun unthaw (f as (a, S)) =
-      (case AList.lookup (op =) fmap' a of
-        NONE => TVar f
-      | SOME (b, _) => TFree (b, S))
+    fun unthaw v =
+      (case AList.lookup (op =) fmap' v of
+        NONE => TVar v
+      | SOME w => TFree w)
   in map_types (map_type_tvar unthaw) t end
 
 

--- a/src/Pure/Proof/proof_checker.ML	Tue Dec 05 20:07:52 2023 +0100
+++ b/src/Pure/Proof/proof_checker.ML	Tue Dec 05 20:56:51 2023 +0100
@@ -78,9 +78,8 @@
         fun thm_of_atom thm Ts =
           let
             val tvars = build_rev (Term.add_tvars (Thm.full_prop_of thm));
-            val (fmap, thm') = Thm.varifyT_global' TFrees.empty thm;
-            val ctye =
-              (tvars @ map (fn ((_, S), ixn) => (ixn, S)) fmap ~~ map (Thm.global_ctyp_of thy) Ts);
+            val (names, thm') = Thm.varifyT_global' TFrees.empty thm;
+            val ctye = tvars @ map #2 names ~~ map (Thm.global_ctyp_of thy) Ts;
           in
             Thm.instantiate (TVars.make ctye, Vars.empty)
               (Thm.forall_intr_vars (Thm.forall_intr_frees thm'))

--- a/src/Pure/proofterm.ML	Tue Dec 05 20:07:52 2023 +0100
+++ b/src/Pure/proofterm.ML	Tue Dec 05 20:56:51 2023 +0100
@@ -121,7 +121,7 @@
   val implies_intr_proof': term -> proof -> proof
   val forall_intr_proof: string * term -> typ option -> proof -> proof
   val forall_intr_proof': term -> proof -> proof
-  val varify_proof: term -> TFrees.set -> proof -> proof
+  val varify_proof: ((string * sort) * (indexname * sort)) list -> proof -> proof
   val legacy_freezeT: term -> proof -> proof
   val rotate_proof: term list -> term -> (string * typ) list -> term list -> int -> proof -> proof
   val permute_prems_proof: term list -> int -> int -> proof -> proof
@@ -932,25 +932,13 @@
 
 (* varify *)
 
-fun varify_names t fixed =
+fun varify_proof names prf =
   let
-    val xs =
-      build (t |> (Term.fold_types o Term.fold_atyps)
-        (fn TFree v => if TFrees.defined fixed v then I else insert (op =) v | _ => I));
-    val used =
-      Name.build_context (t |>
-        (fold_types o fold_atyps) (fn TVar ((a, _), _) => Name.declare a | _ => I));
-    val (ys, _) = fold_map Name.variant (map #1 xs) used;
-    val zs = map2 (fn (_, S) => fn y => ((y, 0), S)) xs ys;
-  in xs ~~ zs end;
-
-fun varify_proof t fixed prf =
-  let
-    val table = TFrees.make (varify_names t fixed);
-    fun varify (a, S) =
-      (case TFrees.lookup table (a, S) of
-        NONE => TFree (a, S)
-      | SOME b => TVar b);
+    val tab = TFrees.make names;
+    fun varify v =
+      (case TFrees.lookup tab v of
+        NONE => TFree v
+      | SOME w => TVar w);
   in map_proof_terms (map_types (map_type_tfree varify)) (map_type_tfree varify) prf end;
 
 

--- a/src/Pure/thm.ML	Tue Dec 05 20:07:52 2023 +0100
+++ b/src/Pure/thm.ML	Tue Dec 05 20:56:51 2023 +0100
@@ -169,7 +169,7 @@
   val trivial: cterm -> thm
   val of_class: ctyp * class -> thm
   val unconstrainT: thm -> thm
-  val varifyT_global': TFrees.set -> thm -> ((string * sort) * indexname) list * thm
+  val varifyT_global': TFrees.set -> thm -> ((string * sort) * (indexname * sort)) list * thm
   val varifyT_global: thm -> thm
   val legacy_freezeT: thm -> thm
   val plain_prop_of: thm -> term
@@ -1934,7 +1934,7 @@
     val (al, prop2) = Type.varify_global tfrees prop1;
     val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
   in
-    (al, Thm (deriv_rule1 (Proofterm.varify_proof prop tfrees, ZTerm.todo_proof) der,
+    (al, Thm (deriv_rule1 (Proofterm.varify_proof al, ZTerm.todo_proof) der,
      {cert = cert,
       tags = [],
       maxidx = Int.max (0, maxidx),

--- a/src/Pure/type.ML	Tue Dec 05 20:07:52 2023 +0100
+++ b/src/Pure/type.ML	Tue Dec 05 20:56:51 2023 +0100
@@ -61,7 +61,8 @@
   val strip_sorts: typ -> typ
   val strip_sorts_dummy: typ -> typ
   val no_tvars: typ -> typ
-  val varify_global: TFrees.set -> term -> ((string * sort) * indexname) list * term
+  val varify_global_names: TFrees.set -> term -> ((string * sort) * (indexname * sort)) list
+  val varify_global: TFrees.set -> term -> ((string * sort) * (indexname * sort)) list * term
   val legacy_freeze_thaw_type: typ -> typ * (typ -> typ)
   val legacy_freeze_type: typ -> typ
   val legacy_freeze_thaw: term -> term * (term -> term)
@@ -353,20 +354,26 @@
 
 (* varify_global *)
 
-fun varify_global fixed t =
+fun varify_global_names fixed t =
   let
-    val fs =
+    val xs =
       build (t |> (Term.fold_types o Term.fold_atyps)
         (fn TFree v => if TFrees.defined fixed v then I else insert (op =) v | _ => I));
     val used =
       Name.build_context (t |>
         (fold_types o fold_atyps) (fn TVar ((a, _), _) => Name.declare a | _ => I));
-    val fmap = fs ~~ map (rpair 0) (#1 (fold_map Name.variant (map fst fs) used));
-    fun thaw (f as (_, S)) =
-      (case AList.lookup (op =) fmap f of
-        NONE => TFree f
-      | SOME xi => TVar (xi, S));
-  in (fmap, map_types (map_type_tfree thaw) t) end;
+    val ys = #1 (fold_map Name.variant (map #1 xs) used);
+  in map2 (fn (a, S) => fn b => ((a, S), ((b, 0), S))) xs ys end;
+
+fun varify_global fixed t =
+  let
+    val names = varify_global_names fixed t;
+    val tab = TFrees.make names;
+    fun get v =
+      (case TFrees.lookup tab v of
+        NONE => TFree v
+      | SOME w => TVar w);
+  in (names, (map_types o map_type_tfree) get t) end;
 
 
 (* freeze_thaw: freeze TVars in a term; return the "thaw" inverse *)