modernized handling of variables

--- a/src/Tools/Code/code_haskell.ML	Sun Mar 27 19:27:54 2022 +0000
+++ b/src/Tools/Code/code_haskell.ML	Mon Mar 28 12:54:09 2022 +0000
@@ -146,8 +146,7 @@
                 val vars = reserved
                   |> intro_base_names_for (is_none o const_syntax)
                       deresolve (t :: ts)
-                  |> intro_vars ((fold o Code_Thingol.fold_varnames)
-                      (insert (op =)) ts []);
+                  |> intro_vars (build (fold Code_Thingol.add_varnames ts));
               in
                 semicolon (
                   (str o deresolve_const) const

--- a/src/Tools/Code/code_ml.ML	Sun Mar 27 19:27:54 2022 +0000
+++ b/src/Tools/Code/code_ml.ML	Mon Mar 28 12:54:09 2022 +0000
@@ -195,8 +195,7 @@
                 val vars = reserved
                   |> intro_base_names_for (is_none o const_syntax)
                        deresolve (t :: ts)
-                  |> intro_vars ((fold o Code_Thingol.fold_varnames)
-                       (insert (op =)) ts []);
+                  |> intro_vars (build (fold Code_Thingol.add_varnames ts));
                 val prolog = if needs_typ then
                   concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty]
                     else (concat o map str) [definer, deresolve_const const];
@@ -513,8 +512,7 @@
                 val vars = reserved
                   |> intro_base_names_for (is_none o const_syntax)
                       deresolve (t :: ts)
-                  |> intro_vars ((fold o Code_Thingol.fold_varnames)
-                      (insert (op =)) ts []);
+                  |> intro_vars (build (fold Code_Thingol.add_varnames ts));
               in concat [
                 (Pretty.block o commas)
                   (map (print_term is_pseudo_fun some_thm vars NOBR) ts),
@@ -526,8 +524,7 @@
                     val vars = reserved
                       |> intro_base_names_for (is_none o const_syntax)
                           deresolve (t :: ts)
-                      |> intro_vars ((fold o Code_Thingol.fold_varnames)
-                          (insert (op =)) ts []);
+                      |> intro_vars (build (fold Code_Thingol.add_varnames ts));
                   in
                     concat (
                       (if is_pseudo then [str "()"]

--- a/src/Tools/Code/code_printer.ML	Sun Mar 27 19:27:54 2022 +0000
+++ b/src/Tools/Code/code_printer.ML	Mon Mar 28 12:54:09 2022 +0000
@@ -341,7 +341,7 @@
 
 fun gen_print_bind print_term thm (fxy : fixity) pat vars =
   let
-    val vs = build (Code_Thingol.fold_varnames (insert (op =)) pat);
+    val vs = build (Code_Thingol.add_varnames pat);
     val vars' = intro_vars vs vars;
   in (print_term thm vars' fxy pat, vars') end;
 

--- a/src/Tools/Code/code_scala.ML	Sun Mar 27 19:27:54 2022 +0000
+++ b/src/Tools/Code/code_scala.ML	Mon Mar 28 12:54:09 2022 +0000
@@ -234,8 +234,8 @@
               print_term tyvars false some_thm vars' NOBR t;
             fun print_clause (eq as ((ts, _), (some_thm, _))) =
               let
-                val vars' = intro_vars ((fold o Code_Thingol.fold_varnames)
-                  (insert (op =)) ts []) vars1;
+                val vars' =
+                  intro_vars (build (fold Code_Thingol.add_varnames ts)) vars1;
               in
                 concat [str "case",
                   tuplify (map (print_term tyvars true some_thm vars' NOBR) ts),

--- a/src/Tools/Code/code_thingol.ML	Sun Mar 27 19:27:54 2022 +0000
+++ b/src/Tools/Code/code_thingol.ML	Mon Mar 28 12:54:09 2022 +0000
@@ -62,6 +62,7 @@
   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
@@ -233,6 +234,10 @@
     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)
@@ -253,7 +258,7 @@
       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;
 
@@ -263,7 +268,7 @@
     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;
@@ -289,12 +294,12 @@
       | 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)