src/Pure/name.ML

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