clarified modules;

--- a/src/Pure/proofterm.ML	Wed Dec 06 15:45:22 2023 +0100
+++ b/src/Pure/proofterm.ML	Wed Dec 06 15:58:20 2023 +0100
@@ -947,32 +947,14 @@
     in Same.commit (map_proof_types_same typ) prf end;
 
 
-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, sort) =
-  (case AList.lookup (op =) alist ix of
-    NONE => TVar (ix, sort)
-  | SOME name => TFree (name, sort));
-
-in
+(* freeze *)
 
 fun legacy_freezeT t prf =
-  let
-    val used = Term.add_tfree_names t [];
-    val (alist, _) = fold_rev new_name (map #1 (Term.add_tvars t [])) ([], used);
-  in
-    (case alist of
-      [] => prf (*nothing to do!*)
-    | _ =>
-        let val frzT = map_type_tvar (freeze_one alist)
-        in map_proof_terms (map_types frzT) frzT prf end)
-  end;
-
-end;
+  (case Type.legacy_freezeT t of
+    NONE => prf
+  | SOME f =>
+      let val frzT = map_type_tvar (fn v => (case f v of NONE => TVar v | SOME T => T))
+      in map_proof_terms (map_types frzT) frzT prf end);
 
 
 (* rotate assumptions *)

--- 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