src/Tools/Code/code_thingol.ML

   val contains_dict_var: iterm -> bool
   val unambiguous_dictss: dict list list -> bool
   val add_constsyms: iterm -> Code_Symbol.T list -> Code_Symbol.T list
   val add_tyconames: iterm -> string list -> string list
   val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
+  val add_varnames: iterm -> string list -> string list
 
   datatype stmt =
       NoStmt
     | Fun of (typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option
     | Datatype of vname list *

         and fold_clause vs (p, t) = fold_term (add_vars p vs) t;
       in fold_term [] end
     fun add_vars t = fold_aux add_vars (insert (op =)) t;
   in fold_aux add_vars f end;
 
+val add_varnames = fold_varnames (insert (op =));
+
+val declare_varnames = fold_varnames Name.declare;
+
 fun exists_var t v = fold_varnames (fn w => fn b => v = w orelse b) t false;
 
 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)], ... } =>

       let
         val (vs_tys, t') = unfold_abs_eta tys t;
       in (v_ty :: vs_tys, t') end
   | unfold_abs_eta tys t =
       let
-        val ctxt = fold_varnames Name.declare t Name.context;
+        val ctxt = Name.build_context (declare_varnames t);
         val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
       in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
 
 fun eta_expand k (const as { dom = tys, ... }, ts) =
   let
     val j = length ts;
     val l = k - j;
     val _ = if l > length tys
       then error "Impossible eta-expansion" else ();
-    val vars = (fold o fold_varnames) Name.declare ts Name.context;
+    val vars = Name.build_context (fold declare_varnames ts);
     val vs_tys = (map o apfst) SOME
       (Name.invent_names vars "a" ((take l o drop j) tys));
   in vs_tys `|==> IConst const `$$ ts @ map (IVar o fst) vs_tys end;
 
 fun map_terms_bottom_up f (t as IConst _) = f t

           then []
           else [(pat_args, body)]
       | distill vs_map pat_args
         (body as ICase { term = IVar (SOME v), clauses = clauses, ... }) =
           let
-            val vs = build ((fold o fold_varnames) (insert (op =)) pat_args);
+            val vs = build (fold add_varnames pat_args);
             fun varnames_disjunctive pat =
-              null (inter (op =) vs (build (fold_varnames (insert (op =)) pat)));
+              null (inter (op =) vs (build (add_varnames pat)));
             fun purge_unused_vars_in t =
               let
-                val vs = build (fold_varnames (insert (op =)) t);
+                val vs = build (add_varnames t);
               in
                 map_terms_bottom_up (fn IVar (SOME v) =>
                   IVar (if member (op =) vs v then SOME v else NONE) | t => t)
               end;
           in