clarified signature;

--- a/src/Pure/Proof/proof_checker.ML	Sat Oct 02 12:45:51 2021 +0200
+++ b/src/Pure/Proof/proof_checker.ML	Sat Oct 02 12:59:16 2021 +0200
@@ -72,7 +72,8 @@
   let val lookup = lookup_thm thy in
     fn prf =>
       let
-        val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees prf Name.context;
+        val prf_names =
+          Name.build_context (prf |> Proofterm.fold_proof_terms Term.declare_term_frees);
 
         fun thm_of_atom thm Ts =
           let

--- a/src/Pure/name.ML	Sat Oct 02 12:45:51 2021 +0200
+++ b/src/Pure/name.ML	Sat Oct 02 12:59:16 2021 +0200
@@ -23,6 +23,7 @@
   val clean: string -> string
   type context
   val context: context
+  val build_context: (context -> context) -> context
   val make_context: string list -> context
   val declare: string -> context -> context
   val is_declared: context -> string -> bool
@@ -104,7 +105,10 @@
 fun declared (Context tab) = Symtab.lookup tab;
 
 val context = Context Symtab.empty |> fold declare ["", "'"];
-fun make_context used = fold declare used context;
+
+fun build_context (f: context -> context) = f context;
+
+val make_context = build_context o fold declare;
 
 
 (* invent names *)

--- a/src/Pure/proofterm.ML	Sat Oct 02 12:45:51 2021 +0200
+++ b/src/Pure/proofterm.ML	Sat Oct 02 12:59:16 2021 +0200
@@ -904,8 +904,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 ~~ #1 (fold_map Name.variant (map fst fs) used);
     fun thaw (a, S) =
       (case AList.lookup (op =) fmap (a, S) of

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

--- a/src/Tools/Code/code_thingol.ML	Sat Oct 02 12:45:51 2021 +0200
+++ b/src/Tools/Code/code_thingol.ML	Sat Oct 02 12:59:16 2021 +0200
@@ -746,7 +746,7 @@
     let
       val k = length ts;
       val tys = (take (num_args - k) o drop k o fst o strip_type) ty;
-      val names = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
+      val names = Name.build_context (ts |> (fold o fold_aterms) Term.declare_term_frees);
       val vs = Name.invent_names names "a" tys;
     in
       fold_map (translate_typ ctxt algbr eqngr permissive) tys