diff -r 1cdc685fe852 -r bf51996ba8c6 src/Pure/type.ML
--- a/src/Pure/type.ML	Wed Dec 06 15:45:22 2023 +0100
+++ b/src/Pure/type.ML	Wed Dec 06 15:58:20 2023 +0100
@@ -63,6 +63,7 @@
   val no_tvars: typ -> typ
   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_freezeT: term -> ((string * int) * sort -> typ option) option
   val legacy_freeze_thaw_type: typ -> typ * (typ -> typ)
   val legacy_freeze_type: typ -> typ
   val legacy_freeze_thaw: term -> term * (term -> term)
@@ -376,6 +377,28 @@
   in (names, (map_types o map_type_tfree) get t) end;
 
 
+(* legacy_freezeT *)
+
+local
+
+fun new_name ix (pairs, used) =
+  let val v = singleton (Name.variant_list used) (string_of_indexname ix)
+  in ((ix, v) :: pairs, v :: used) end;
+
+fun freeze_one alist (ix, S) =
+  AList.lookup (op =) alist ix |> Option.map (fn a => TFree (a, S));
+
+in
+
+fun legacy_freezeT t =
+  let
+    val used = Term.add_tfree_names t [];
+    val (alist, _) = fold_rev new_name (map #1 (Term.add_tvars t [])) ([], used);
+  in if null alist then NONE else SOME (freeze_one alist) end;
+
+end;
+
+
 (* freeze_thaw: freeze TVars in a term; return the "thaw" inverse *)
 
 local