--- a/src/Pure/type.ML Sat Oct 02 12:45:51 2021 +0200
+++ b/src/Pure/type.ML Sat Oct 02 12:59:16 2021 +0200
@@ -358,8 +358,9 @@
val fs =
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.context
- |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
+ 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