# HG changeset patch
# User wenzelm
# Date 1733174189 -3600
# Node ID 5335b1ca6233d74aadeb8aad60ee4cbbc39b476f
# Parent  58073f3d748a27b7e463499beb16ca23a65f4aad
more elementary operation Term.variant_bounds: only for bounds vs. frees, no consts, no tfrees;

diff -r 58073f3d748a -r 5335b1ca6233 src/HOL/Library/conditional_parametricity.ML
--- a/src/HOL/Library/conditional_parametricity.ML	Mon Dec 02 20:35:12 2024 +0100
+++ b/src/HOL/Library/conditional_parametricity.ML	Mon Dec 02 22:16:29 2024 +0100
@@ -246,7 +246,7 @@
     val i = maxidx_of_term t + 1;
     fun tvar_to_tfree ((name, _), sort) = (name, sort);
     val tvars = Term.add_tvars t [];
-    val new_frees = map TFree (Term.variant_frees t (map tvar_to_tfree tvars));
+    val new_frees = map TFree (Term.variant_bounds t (map tvar_to_tfree tvars));
     val u = subst_atomic_types ((map TVar tvars) ~~ new_frees) t;
     val T = fastype_of t;
     val U = fastype_of u;
diff -r 58073f3d748a -r 5335b1ca6233 src/HOL/Library/refute.ML
--- a/src/HOL/Library/refute.ML	Mon Dec 02 20:35:12 2024 +0100
+++ b/src/HOL/Library/refute.ML	Mon Dec 02 22:16:29 2024 +0100
@@ -1186,7 +1186,7 @@
           (a, T) :: strip_all_vars t
       | strip_all_vars _ = [] : (string * typ) list
     val strip_t = strip_all_body ex_closure
-    val frees = Term.variant_frees strip_t (strip_all_vars ex_closure)
+    val frees = Term.variant_bounds strip_t (strip_all_vars ex_closure)
     val subst_t = Term.subst_bounds (map Free (rev frees), strip_t)
   in
     find_model ctxt (actual_params ctxt params) assm_ts subst_t true
diff -r 58073f3d748a -r 5335b1ca6233 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Mon Dec 02 20:35:12 2024 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Mon Dec 02 22:16:29 2024 +0100
@@ -245,7 +245,7 @@
              if null (preds_of ps prem) then prem
              else lift_prem prem) prems,
            HOLogic.mk_Trueprop (lift_pred p ts));
-        val vs = map (Var o apfst (rpair 0)) (Term.variant_frees prem params')
+        val vs = map (Var o apfst (rpair 0)) (Term.variant_bounds prem params')
       in
         (Logic.list_all (params', prem), (vs, subst_bounds (rev vs, prem)))
       end) prems);
diff -r 58073f3d748a -r 5335b1ca6233 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Mon Dec 02 20:35:12 2024 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Mon Dec 02 22:16:29 2024 +0100
@@ -146,7 +146,7 @@
   in Option.map prove (map_term f prop (the_default prop opt)) end;
 
 fun abs_params params t =
-  let val vs =  map (Var o apfst (rpair 0)) (Term.variant_frees t params)
+  let val vs =  map (Var o apfst (rpair 0)) (Term.variant_bounds t params)
   in (Logic.list_all (params, t), (vs, subst_bounds (rev vs, t))) end;
 
 fun inst_params thy (vs, p) th cts =
diff -r 58073f3d748a -r 5335b1ca6233 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Mon Dec 02 20:35:12 2024 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Mon Dec 02 22:16:29 2024 +0100
@@ -156,7 +156,7 @@
             let
               val recs = filter (Old_Datatype_Aux.is_rec_type o snd) (cargs' ~~ cargs);
               val rargs = map (rpair dummyT o fst o fst) recs;
-              val subs = Term.variant_frees rhs rargs;
+              val subs = Term.variant_bounds rhs rargs;
               val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
                 (Free x, (Old_Datatype_Aux.body_index y, Free z))) recs subs) rhs (fnames', fnss')
                   handle RecError s => primrec_eq_err lthy s eq
diff -r 58073f3d748a -r 5335b1ca6233 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Dec 02 20:35:12 2024 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Dec 02 22:16:29 2024 +0100
@@ -391,10 +391,10 @@
         |> map_filter (try (apsnd (fn Nested_Rec p => p)));
 
       fun ensure_unique frees t =
-        if member (op =) frees t then Free (the_single (Term.variant_frees t [dest_Free t])) else t;
+        if member (op =) frees t then Free (the_single (Term.variant_bounds t [dest_Free t])) else t;
 
       val args = replicate n_args ("", dummyT)
-        |> Term.variant_frees t
+        |> Term.variant_bounds t
         |> rev
         |> map Free
         |> fold (fn (ctr_arg_idx, (arg_idx, _)) =>
diff -r 58073f3d748a -r 5335b1ca6233 src/HOL/Tools/Old_Datatype/old_primrec.ML
--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Mon Dec 02 20:35:12 2024 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Mon Dec 02 22:16:29 2024 +0100
@@ -149,7 +149,7 @@
           let
             val recs = filter (Old_Datatype_Aux.is_rec_type o snd) (cargs' ~~ cargs);
             val rargs = map (rpair dummyT o fst o fst) recs;
-            val subs = Term.variant_frees rhs rargs;
+            val subs = Term.variant_bounds rhs rargs;
             val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
               (Free x, (Old_Datatype_Aux.body_index y, Free z))) recs subs) rhs (fnames', fnss')
                 handle PrimrecError (s, NONE) => primrec_error_eqn s eq
diff -r 58073f3d748a -r 5335b1ca6233 src/Provers/preorder.ML
--- a/src/Provers/preorder.ML	Mon Dec 02 20:35:12 2024 +0100
+++ b/src/Provers/preorder.ML	Mon Dec 02 22:16:29 2024 +0100
@@ -555,7 +555,7 @@
 fun trans_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
  let
   val thy = Proof_Context.theory_of ctxt;
-  val rfrees = map Free (rev (Term.variant_frees A (Logic.strip_params A)));
+  val rfrees = map Free (rev (Term.variant_bounds A (Logic.strip_params A)));
   val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
   val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
   val lesss = flat (map_index (mkasm_trans thy o swap) Hs);
@@ -578,7 +578,7 @@
 fun quasi_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
  let
   val thy = Proof_Context.theory_of ctxt
-  val rfrees = map Free (rev (Term.variant_frees A (Logic.strip_params A)));
+  val rfrees = map Free (rev (Term.variant_bounds A (Logic.strip_params A)));
   val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
   val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
   val lesss = flat (map_index (mkasm_quasi thy o swap) Hs);
diff -r 58073f3d748a -r 5335b1ca6233 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Mon Dec 02 20:35:12 2024 +0100
+++ b/src/Pure/consts.ML	Mon Dec 02 22:16:29 2024 +0100
@@ -313,7 +313,7 @@
 fun rev_abbrev lhs rhs =
   let
     val (xs, body) = strip_abss (Envir.beta_eta_contract rhs);
-    val vars = map (fn (x, T) => Var ((x, 0), T)) (Term.variant_frees body xs);
+    val vars = map (fn (x, T) => Var ((x, 0), T)) (Term.variant_bounds body xs);
   in (Term.subst_bounds (rev vars, body), Term.list_comb (lhs, vars)) end;
 
 in
diff -r 58073f3d748a -r 5335b1ca6233 src/Pure/primitive_defs.ML
--- a/src/Pure/primitive_defs.ML	Mon Dec 02 20:35:12 2024 +0100
+++ b/src/Pure/primitive_defs.ML	Mon Dec 02 22:16:29 2024 +0100
@@ -77,7 +77,7 @@
 fun abs_def eq =
   let
     val body = Term.strip_all_body eq;
-    val vars = map Free (Term.variant_frees body (Term.strip_all_vars eq));
+    val vars = map Free (Term.variant_bounds body (Term.strip_all_vars eq));
     val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (rev vars, body));
     val (lhs', args) = Term.strip_comb lhs;
     val rhs' = fold_rev (absfree o dest_Free) args rhs;
diff -r 58073f3d748a -r 5335b1ca6233 src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Dec 02 20:35:12 2024 +0100
+++ b/src/Pure/term.ML	Mon Dec 02 22:16:29 2024 +0100
@@ -157,6 +157,7 @@
   val declare_tvar_names: (int -> bool) -> term -> Name.context -> Name.context
   val declare_free_names: term -> Name.context -> Name.context
   val declare_var_names: (int -> bool) -> term -> Name.context -> Name.context
+  val variant_bounds: term -> (string * 'a) list -> (string * 'a) list
   val hidden_polymorphism: term -> (indexname * sort) list
   val declare_term_names: term -> Name.context -> Name.context
   val variant_frees: term -> (string * 'a) list -> (string * 'a) list
@@ -583,6 +584,8 @@
 val declare_free_names = fold_aterms (fn Free (x, _) => Name.declare x | _ => I);
 fun declare_var_names pred = fold_aterms (fn Var ((x, i), _) => pred i ? Name.declare x | _ => I);
 
+fun variant_bounds t = Name.variant_names_build (declare_free_names t);
+
 (*extra type variables in a term, not covered by its type*)
 fun hidden_polymorphism t =
   let