# HG changeset patch
# User wenzelm
# Date 1732966218 -3600
# Node ID 1052f79afe217f859bb70ce1c1f1f8cee07a3ac3
# Parent  08574da77b4ae60de7708320ef50a96697e2b5d2
tuned: more direct use of Name.context operations;

diff -r 08574da77b4a -r 1052f79afe21 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Fri Nov 29 17:40:15 2024 +0100
+++ b/src/Tools/Code/code_thingol.ML	Sat Nov 30 12:30:18 2024 +0100
@@ -255,9 +255,6 @@
 
 fun exists_var t v = fold_varnames (fn w => fn b => v = w orelse b) t false;
 
-fun invent_params used tys =
-  Name.invent_names (Name.build_context used) "a" tys;
-
 fun split_pat_abs ((NONE, ty) `|=> (t, _)) = SOME ((IVar NONE, ty), t)
   | split_pat_abs ((SOME v, ty) `|=> (t, _)) = SOME (case t
      of ICase { term = IVar (SOME w), clauses = [(p, body)], ... } =>
@@ -276,7 +273,8 @@
       in (v :: vs, t') end
   | unfold_abs_eta tys t =
       let
-        val vs = map (SOME o fst) (invent_params (declare_varnames t) tys);
+        val names = Name.build_context (declare_varnames t);
+        val vs = map SOME (Name.invent names "a" (length tys));
       in (vs, t `$$ map IVar vs) end;
 
 fun satisfied_application wanted ({ dom, range, ... }, ts) =
@@ -293,9 +291,8 @@
       in (([], (ts1, rty)), ts2) end
     else
       let
-        val vs_tys = invent_params (fold declare_varnames ts)
-          (((take delta o drop given) dom))
-          |> (map o apfst) SOME;
+        val names = Name.build_context (fold declare_varnames ts);
+        val vs_tys = (map o apfst) SOME (Name.invent_names names "a" (take delta (drop given dom)));
       in ((vs_tys, (ts @ map (IVar o fst) vs_tys, rty)), []) end
   end