tuned signature: more operations;

--- a/src/HOL/Tools/functor.ML	Sat Nov 30 13:41:38 2024 +0100
+++ b/src/HOL/Tools/functor.ML	Sat Nov 30 16:01:58 2024 +0100
@@ -98,13 +98,9 @@
       (if co then [false] else []) @ (if contra then [true] else [])) variances;
     val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances);
     val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances);
-    fun invents n k nctxt =
-      let
-        val names = Name.invent nctxt n k;
-      in (names, fold Name.declare names nctxt) end;
     val ((names21, names32), nctxt) = Variable.names_of ctxt
-      |> invents "f" (length Ts21)
-      ||>> invents "f" (length Ts32);
+      |> Name.invent' "f" (length Ts21)
+      ||>> Name.invent' "f" (length Ts32);
     val T1 = Type (tyco, Ts1);
     val T2 = Type (tyco, Ts2);
     val T3 = Type (tyco, Ts3);

--- a/src/Pure/name.ML	Sat Nov 30 13:41:38 2024 +0100
+++ b/src/Pure/name.ML	Sat Nov 30 16:01:58 2024 +0100
@@ -29,6 +29,7 @@
   val declare_renamed: string * string -> context -> context
   val is_declared: context -> string -> bool
   val invent: context -> string -> int -> string list
+  val invent': string -> int -> context -> string list * context
   val invent_global: string -> int -> string list
   val invent_global_types: int -> string list
   val invent_names: context -> string -> 'a list -> (string * 'a) list
@@ -131,6 +132,10 @@
           in if is_declared ctxt x then invs x' n else x :: invs x' (n - 1) end;
   in invs o clean end;
 
+fun invent' x n ctxt =
+  let val xs = invent ctxt x n
+  in (xs, fold declare xs ctxt) end;
+
 val invent_global = invent context;
 val invent_global_types = invent_global aT;
 

--- a/src/Pure/type_infer.ML	Sat Nov 30 13:41:38 2024 +0100
+++ b/src/Pure/type_infer.ML	Sat Nov 30 16:01:58 2024 +0100
@@ -109,9 +109,7 @@
 
     fun subst_param (xi, S) (inst, used) =
       if is_param xi then
-        let
-          val [a] = Name.invent used Name.aT 1;
-          val used' = Name.declare a used;
+        let val ([a], used') = Name.invent' Name.aT 1 used;
         in (TVars.add ((xi, S), TFree (a, improve_sort S)) inst, used') end
       else (inst, used);
     val params = TVars.build (fold TVars.add_tvars ts) |> TVars.list_set;

--- a/src/Tools/nbe.ML	Sat Nov 30 13:41:38 2024 +0100
+++ b/src/Tools/nbe.ML	Sat Nov 30 16:01:58 2024 +0100
@@ -339,11 +339,8 @@
         val vs = (fold o Code_Thingol.fold_varnames)
           (fn v => AList.map_default (op =) (v, 0) (Integer.add 1)) args [];
         val names = Name.make_context (map fst vs);
-        fun declare v k ctxt =
-          let val vs = Name.invent ctxt v k
-          in (vs, fold Name.declare vs ctxt) end;
         val (vs_renames, _) = fold_map (fn (v, k) => if k > 1
-          then declare v (k - 1) #>> (fn vs => (v, vs))
+          then Name.invent' v (k - 1) #>> (fn vs => (v, vs))
           else pair (v, [])) vs names;
         val samepairs = maps (fn (v, vs) => map (pair v) vs) vs_renames;
         fun subst_vars (t as IConst _) samepairs = (t, samepairs)