src/Pure/type.ML

--- a/src/Pure/type.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/type.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -61,7 +61,7 @@
   val strip_sorts: typ -> typ
   val strip_sorts_dummy: typ -> typ
   val no_tvars: typ -> typ
-  val varify_global: Term_Subst.TFrees.set -> term -> ((string * sort) * indexname) list * term
+  val varify_global: TFrees.set -> term -> ((string * sort) * indexname) 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)
@@ -357,7 +357,7 @@
   let
     val fs =
       build (t |> (Term.fold_types o Term.fold_atyps)
-        (fn TFree v => if Term_Subst.TFrees.defined fixed v then I else insert (op =) v | _ => I));
+        (fn TFree v => if TFrees.defined fixed v then I else insert (op =) v | _ => I));
     val used = Name.context
       |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
     val fmap = fs ~~ map (rpair 0) (#1 (fold_map Name.variant (map fst fs) used));