# HG changeset patch
# User wenzelm
# Date 1733488405 -3600
# Node ID fa37ee54644c4b3b9dd6fcb93d7ee07c0c7f409b
# Parent  e2ab4147b244b50d1a4ba2f4dd89ce1378dadf25
clarified printing of consts: rename apart from all bounds, and thus avoid old Term.declare_free_names with its adhoc policy ("as they are printed");

diff -r e2ab4147b244 -r fa37ee54644c src/HOL/Auth/Guard/Proto.thy
--- a/src/HOL/Auth/Guard/Proto.thy	Tue Dec 03 22:46:24 2024 +0100
+++ b/src/HOL/Auth/Guard/Proto.thy	Fri Dec 06 13:33:25 2024 +0100
@@ -464,7 +464,7 @@
 apply (frule Guard_safe, simp)
 apply (frule Crypt_guard_invKey, simp)
 apply (frule ok_Guard, simp, simp, simp, clarsimp)
-apply (frule_tac K="pubK' s b" in Crypt_guard_invKey, simp)
+apply (frule_tac K="pubK' s Proto.b" in Crypt_guard_invKey, simp)
 apply (frule_tac R=ns1 and R'=ns1 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
 apply (simp add: secret_def, simp add: secret_def, force, force)
 apply (simp add: secret_def keys_def, blast)
@@ -475,7 +475,7 @@
 apply (frule Guard_safe, simp)
 apply (frule Crypt_guard_invKey, simp)
 apply (frule_tac x=ns3b in ok_Guard, simp, simp, simp, clarsimp)
-apply (frule_tac K="pubK' s a" in Crypt_guard_invKey, simp)
+apply (frule_tac K="pubK' s Proto.a" in Crypt_guard_invKey, simp)
 apply (frule_tac R=ns1 and R'=ns2 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
 apply (simp add: secret_def, simp add: secret_def, force, force)
 apply (simp add: secret_def, rule No_Nonce, simp)
@@ -493,7 +493,7 @@
 apply (frule Guard_safe, simp)
 apply (frule Crypt_guard_invKey, simp)
 apply (frule ok_Guard, simp, simp, simp, clarsimp)
-apply (frule_tac K="pubK' s b" in Crypt_guard_invKey, simp)
+apply (frule_tac K="pubK' s Proto.b" in Crypt_guard_invKey, simp)
 apply (frule_tac R=ns2 and R'=ns1 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
 apply (simp add: secret_def, simp add: secret_def, force, force)
 apply (simp add: secret_def, rule No_Nonce, simp)
@@ -503,7 +503,7 @@
 apply (frule Guard_safe, simp)
 apply (frule Crypt_guard_invKey, simp)
 apply (frule_tac x=ns3b in ok_Guard, simp, simp, simp, clarsimp)
-apply (frule_tac K="pubK' s a" in Crypt_guard_invKey, simp)
+apply (frule_tac K="pubK' s Proto.a" in Crypt_guard_invKey, simp)
 apply (frule_tac R=ns2 and R'=ns2 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
 apply (simp add: secret_def, simp add: secret_def, force, force)
 apply (simp add: secret_def keys_def, blast)
diff -r e2ab4147b244 -r fa37ee54644c src/HOL/Hoare_Parallel/RG_Examples.thy
--- a/src/HOL/Hoare_Parallel/RG_Examples.thy	Tue Dec 03 22:46:24 2024 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Examples.thy	Fri Dec 06 13:33:25 2024 +0100
@@ -117,11 +117,11 @@
     apply simp
    apply clarify
    apply simp
-   apply(subgoal_tac "xa=0")
+   apply(subgoal_tac "x=0")
     apply simp
    apply arith
   apply clarify
-  apply(case_tac xaa, simp, simp)
+  apply(case_tac xa, simp, simp)
  apply clarify
  apply simp
  apply(erule_tac x=0 in all_dupE)
diff -r e2ab4147b244 -r fa37ee54644c src/HOL/Nominal/Examples/Class2.thy
--- a/src/HOL/Nominal/Examples/Class2.thy	Tue Dec 03 22:46:24 2024 +0100
+++ b/src/HOL/Nominal/Examples/Class2.thy	Fri Dec 06 13:33:25 2024 +0100
@@ -4671,7 +4671,7 @@
 apply(drule_tac pi="[(x,za)]" and x="(x):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
 apply(simp add: CAND_eqvt_name calc_atm)
 apply(auto intro: CANDs_alpha)[1]
-apply(drule_tac pi="[(x,za)]" and x="(x):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(x,za)]" and x="(x):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
 apply(simp add: CAND_eqvt_name calc_atm)
 apply(auto intro: CANDs_alpha)[1]
 apply(drule_tac pi="[(x,za)]" and x="(x):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
@@ -4679,17 +4679,17 @@
 apply(auto intro: CANDs_alpha)[1]
 apply(case_tac "x=ya")
 apply(simp)
-apply(drule_tac pi="[(ya,za)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(ya,za)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
 apply(simp add: CAND_eqvt_name calc_atm)
 apply(auto intro: CANDs_alpha)[1]
 apply(simp)
 apply(case_tac "za=ya")
 apply(simp)
-apply(drule_tac pi="[(x,ya)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(x,ya)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
 apply(simp add: CAND_eqvt_name calc_atm)
 apply(auto intro: CANDs_alpha)[1]
 apply(simp)
-apply(drule_tac pi="[(x,za)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(x,za)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
 apply(simp add: CAND_eqvt_name calc_atm)
 apply(auto intro: CANDs_alpha)[1]
 apply(case_tac "x=xa")
@@ -4707,7 +4707,7 @@
 apply(drule_tac pi="[(x,za)]" and x="(xa):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
 apply(simp add: CAND_eqvt_name calc_atm)
 apply(auto intro: CANDs_alpha)[1]
-apply(drule_tac pi="[(x,za)]" and x="(x):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(x,za)]" and x="(x):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
 apply(simp add: CAND_eqvt_name calc_atm)
 apply(auto intro: CANDs_alpha)[1]
 apply(case_tac "x=xa")
@@ -4727,17 +4727,17 @@
 apply(auto intro: CANDs_alpha)[1]
 apply(case_tac "x=ya")
 apply(simp)
-apply(drule_tac pi="[(ya,za)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(ya,za)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
 apply(simp add: CAND_eqvt_name calc_atm)
 apply(auto intro: CANDs_alpha)[1]
 apply(simp)
 apply(case_tac "za=ya")
 apply(simp)
-apply(drule_tac pi="[(x,ya)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(x,ya)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
 apply(simp add: CAND_eqvt_name calc_atm)
 apply(auto intro: CANDs_alpha)[1]
 apply(simp)
-apply(drule_tac pi="[(x,za)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(x,za)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
 apply(simp add: CAND_eqvt_name calc_atm)
 apply(auto intro: CANDs_alpha)[1]
 done
@@ -4800,7 +4800,7 @@
 apply(drule_tac pi="[(x,y)]" and x="<aa>:Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
 apply(simp add: CAND_eqvt_name calc_atm)
 apply(auto intro: CANDs_alpha)[1]
-apply(drule_tac pi="[(x,y)]" and x="(x):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(x,y)]" and x="(x):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
 apply(simp add: CAND_eqvt_name calc_atm)
 apply(auto intro: CANDs_alpha)[1]
 apply(drule_tac pi="[(x,y)]" and x="<aa>:Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
@@ -4808,17 +4808,17 @@
 apply(auto intro: CANDs_alpha)[1]
 apply(case_tac "x=xa")
 apply(simp)
-apply(drule_tac pi="[(xa,y)]" and x="(xa):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(xa,y)]" and x="(xa):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
 apply(simp add: CAND_eqvt_name calc_atm)
 apply(auto intro: CANDs_alpha)[1]
 apply(simp)
 apply(case_tac "y=xa")
 apply(simp)
-apply(drule_tac pi="[(x,xa)]" and x="(xa):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(x,xa)]" and x="(xa):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
 apply(simp add: CAND_eqvt_name calc_atm)
 apply(auto intro: CANDs_alpha)[1]
 apply(simp)
-apply(drule_tac pi="[(x,y)]" and x="(xa):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(x,y)]" and x="(xa):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
 apply(simp add: CAND_eqvt_name calc_atm)
 apply(auto intro: CANDs_alpha)[1]
 done
diff -r e2ab4147b244 -r fa37ee54644c src/HOL/Tools/Ctr_Sugar/case_translation.ML
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Tue Dec 03 22:46:24 2024 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Fri Dec 06 13:33:25 2024 +0100
@@ -477,7 +477,7 @@
                 map (pair "x") (drop j (take i (binder_types (fastype_of t)))), [])
               else chop i zs;
             val u = fold_rev Term.abs ys (strip_abs_body t);
-            val xs' = map Free (Name.variant_names (Term.declare_term_names u used) xs);
+            val xs' = map Free (Name.variant_names (Term.declare_free_names u used) xs);
             val (xs1, xs2) = chop j xs'
           in (xs', list_comb (subst_bounds (rev xs1, u), xs2)) end;
         fun is_dependent i t =
diff -r e2ab4147b244 -r fa37ee54644c src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Dec 03 22:46:24 2024 +0100
+++ b/src/Pure/Isar/proof_context.ML	Fri Dec 06 13:33:25 2024 +0100
@@ -43,6 +43,8 @@
   val type_space: Proof.context -> Name_Space.T
   val const_space: Proof.context -> Name_Space.T
   val lookup_free: Proof.context -> string -> string option
+  val printable_const: Proof.context -> string -> bool
+  val exclude_consts: Symset.T -> Proof.context -> Proof.context
   val defs_context: Proof.context -> Defs.context
   val intern_class: Proof.context -> xstring -> string
   val intern_type: Proof.context -> xstring -> string
@@ -251,7 +253,8 @@
    {mode: mode,                  (*inner syntax mode*)
     syntax: Local_Syntax.T,      (*local syntax*)
     tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
-    consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
+    consts: Symset.T * Consts.T * Consts.T,
+      (*exclude consts, local/global consts -- local name space / abbrevs only*)
     facts: Facts.T,              (*local facts, based on initial global facts*)
     cases: cases};               (*named case contexts*)
 
@@ -265,7 +268,7 @@
     make_data (mode_default,
       Local_Syntax.init thy,
       (Type.change_ignore (Sign.tsig_of thy), Sign.tsig_of thy),
-      (Consts.change_ignore (Sign.consts_of thy), Sign.consts_of thy),
+      (Symset.empty, Consts.change_ignore (Sign.consts_of thy), Sign.consts_of thy),
       Global_Theory.facts_of thy,
       empty_cases);
 );
@@ -302,6 +305,8 @@
   map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
     (mode, syntax, tsig, f consts, facts, cases));
 
+fun map_local_consts f = map_consts (fn (a, b, c) => (a, f b, c));
+
 fun map_facts_result f =
   map_data_result (fn (mode, syntax, tsig, consts, facts, cases) =>
     let val (res, facts') = f facts
@@ -326,7 +331,8 @@
 fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
 fun arity_sorts ctxt = Type.arity_sorts (Context.Proof ctxt) (tsig_of ctxt);
 
-val consts_of = #1 o #consts o rep_data;
+val exclude_consts_of = #1 o #consts o rep_data;
+val consts_of = #2 o #consts o rep_data;
 val cases_of = #cases o rep_data;
 
 
@@ -373,6 +379,13 @@
         in if not is_const orelse is_free_declared then SOME x else NONE end
     | fixed => fixed);
 
+fun printable_const ctxt x =
+  is_none (lookup_free ctxt x) andalso
+    not (Symset.member (exclude_consts_of ctxt) x);
+
+fun exclude_consts names2 =
+  map_consts (fn (names1, consts, thy_consts) => (Symset.union names1 names2, consts, thy_consts));
+
 
 (* name spaces *)
 
@@ -387,7 +400,7 @@
 
 fun extern_class ctxt = Name_Space.extern ctxt (class_space ctxt);
 fun extern_type ctxt = Name_Space.extern ctxt (type_space ctxt);
-fun extern_const ctxt = Name_Space.extern_if (is_none o lookup_free ctxt) ctxt (const_space ctxt);
+fun extern_const ctxt = Name_Space.extern_if (printable_const ctxt) ctxt (const_space ctxt);
 fun extern_fixed ctxt x = if Name.is_skolem x then Variable.revert_fixed ctxt x else x;
 
 fun extern_entity ctxt =
@@ -422,10 +435,10 @@
         if Type.eq_tsig (thy_tsig, global_tsig) then tsig
         else (Type.merge_tsig (Context.Proof ctxt) (local_tsig, thy_tsig), thy_tsig)  (*historic merge order*)
       end) |>
-    map_consts (fn consts as (local_consts, global_consts) =>
+    map_consts (fn consts as (exclude_consts, local_consts, global_consts) =>
       let val thy_consts = Sign.consts_of thy in
         if Consts.eq_consts (thy_consts, global_consts) then consts
-        else (Consts.merge (local_consts, thy_consts), thy_consts)  (*historic merge order*)
+        else (exclude_consts, Consts.merge (local_consts, thy_consts), thy_consts)  (*historic merge order*)
       end)
   end;
 
@@ -1241,7 +1254,7 @@
 (* aliases *)
 
 fun type_alias b c ctxt = (map_tsig o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt;
-fun const_alias b c ctxt = (map_consts o apfst) (Consts.alias (naming_of ctxt) b c) ctxt;
+fun const_alias b c ctxt = map_local_consts (Consts.alias (naming_of ctxt) b c) ctxt;
 
 
 (* local constants *)
@@ -1251,7 +1264,7 @@
     fun prepT raw_T =
       let val T = cert_typ ctxt raw_T
       in cert_term ctxt (Const (c, T)); T end;
-  in ctxt |> (map_consts o apfst) (Consts.constrain (c, Option.map prepT opt_T)) end;
+  in ctxt |> map_local_consts (Consts.constrain (c, Option.map prepT opt_T)) end;
 
 fun add_abbrev mode (b, raw_t) ctxt =
   let
@@ -1262,12 +1275,12 @@
       |> Consts.abbreviate (Context.Proof ctxt) (tsig_of ctxt) mode (b, t);
   in
     ctxt
-    |> (map_consts o apfst) (K consts')
+    |> map_local_consts (K consts')
     |> Variable.declare_term rhs
     |> pair (lhs, rhs)
   end;
 
-fun revert_abbrev mode c = (map_consts o apfst) (Consts.revert_abbrev mode c);
+fun revert_abbrev mode c = map_local_consts (Consts.revert_abbrev mode c);
 
 fun generic_add_abbrev mode arg =
   Context.mapping_result (Sign.add_abbrev mode arg) (add_abbrev mode arg);
@@ -1506,9 +1519,9 @@
 fun pretty_abbrevs verbose show_globals ctxt =
   let
     val space = const_space ctxt;
-    val (constants, global_constants) =
-      apply2 (#constants o Consts.dest) (#consts (rep_data ctxt));
-    val globals = Symtab.make global_constants;
+    val (_, consts, global_consts) = #consts (rep_data ctxt);
+    val constants = #constants (Consts.dest consts);
+    val globals = Symtab.make (#constants (Consts.dest global_consts));
     fun add_abbr (_, (_, NONE)) = I
       | add_abbr (c, (T, SOME t)) =
           if not show_globals andalso Symtab.defined globals c then I
diff -r e2ab4147b244 -r fa37ee54644c src/Pure/Isar/subgoal.ML
--- a/src/Pure/Isar/subgoal.ML	Tue Dec 03 22:46:24 2024 +0100
+++ b/src/Pure/Isar/subgoal.ML	Fri Dec 06 13:33:25 2024 +0100
@@ -171,7 +171,7 @@
     val subgoal = #1 (Logic.dest_implies (Thm.prop_of st));
     val subgoal_params =
       map (apfst (Name.internal o Name.clean)) (Term.strip_all_vars subgoal)
-      |> Term.variant_frees subgoal |> map #1;
+      |> Term.variant_bounds subgoal |> map #1;
 
     val n = length subgoal_params;
     val m = length raw_param_specs;
diff -r e2ab4147b244 -r fa37ee54644c src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Tue Dec 03 22:46:24 2024 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Dec 06 13:33:25 2024 +0100
@@ -735,15 +735,27 @@
 val typing_elem = YXML.output_markup_elem Markup.typing;
 val sorting_elem = YXML.output_markup_elem Markup.sorting;
 
-fun unparse_t t_to_ast pretty_flags language_markup ctxt t =
+val exclude_consts =
   let
+    fun exclude (Ast.Appl [Ast.Constant "_bound", Ast.Variable x]) = Symset.insert x
+      | exclude (Ast.Appl [Ast.Constant "_free", Ast.Variable x]) = Symset.insert x
+      | exclude (Ast.Appl asts) = fold exclude asts
+      | exclude _ = I;
+  in Proof_Context.exclude_consts o Symset.build o exclude end;
+
+fun unparse_t t_to_ast pretty_flags language_markup ctxt0 t =
+  let
+    val syn = Proof_Context.syntax_of ctxt0;
+    val prtabs = Syntax.print_mode_tabs syn;
+    val trf = Syntax.print_ast_translation syn;
+
+    val ast = t_to_ast ctxt0 (Syntax.print_translation syn) t;
+    val ctxt = exclude_consts ast ctxt0;
+
     val show_markup = Config.get ctxt show_markup;
     val show_sorts = Config.get ctxt show_sorts;
     val show_types = Config.get ctxt show_types orelse show_sorts;
 
-    val syn = Proof_Context.syntax_of ctxt;
-    val prtabs = Syntax.print_mode_tabs syn;
-    val trf = Syntax.print_ast_translation syn;
     val markup = markup_entity_cache ctxt;
     val extern = extern_cache ctxt;
 
@@ -801,8 +813,7 @@
             in Unsynchronized.change cache (Ast.Table.update (A, block)); block end)
       end;
   in
-    t_to_ast ctxt (Syntax.print_translation syn) t
-    |> Ast.normalize ctxt {permissive_constraints = true} (Syntax.print_rules syn)
+    Ast.normalize ctxt {permissive_constraints = true} (Syntax.print_rules syn) ast
     |> pretty_ast pretty_flags language_markup
   end;
 
diff -r e2ab4147b244 -r fa37ee54644c src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Tue Dec 03 22:46:24 2024 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML	Fri Dec 06 13:33:25 2024 +0100
@@ -302,13 +302,13 @@
 fun mark_bound_body (x, T) = Const ("_bound", dummyT) $ Free (x, T);
 
 fun bound_vars vars body =
-  subst_bounds (map mark_bound_abs (rev (Term.variant_frees body vars)), body);
+  subst_bounds (map mark_bound_abs (rev (Term.variant_bounds body vars)), body);
 
 fun strip_abss vars_of body_of tm =
   let
     val vars = vars_of tm;
     val body = body_of tm;
-    val new_vars = Term.variant_frees body vars;
+    val new_vars = Term.variant_bounds body vars;
     fun subst (x, T) b =
       if Name.is_internal x andalso not (Term.is_dependent b)
       then (Const ("_idtdummy", T), incr_boundvars ~1 b)
@@ -322,7 +322,7 @@
     (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm));
 
 fun atomic_abs_tr' (x, T, t) =
-  let val xT = singleton (Term.variant_frees t) (x, T)
+  let val xT = singleton (Term.variant_bounds t) (x, T)
   in (mark_bound_abs xT, subst_bound (mark_bound_body xT, t)) end;
 
 fun abs_ast_tr' asts =
@@ -389,7 +389,7 @@
 (* dependent / nondependent quantifiers *)
 
 fun print_abs (x, T, b) =
-  let val x' = #1 (Name.variant x (Name.build_context (Term.declare_term_names b)))
+  let val x' = #1 (Name.variant x (Name.build_context (Term.declare_free_names b)))
   in (x', subst_bound (mark_bound_abs (x', T), b)) end;
 
 fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
diff -r e2ab4147b244 -r fa37ee54644c src/Pure/type_infer_context.ML
--- a/src/Pure/type_infer_context.ML	Tue Dec 03 22:46:24 2024 +0100
+++ b/src/Pure/type_infer_context.ML	Fri Dec 06 13:33:25 2024 +0100
@@ -248,7 +248,7 @@
         val (Ts_bTs', ts') = Type_Infer.finish ctxt tye (Ts @ map snd bs, ts);
         val (Ts', Ts'') = chop (length Ts) Ts_bTs';
         fun prep t =
-          let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
+          let val xs = rev (Term.variant_bounds t (rev (map fst bs ~~ Ts'')))
           in Term.subst_bounds (map Syntax_Trans.mark_bound_abs xs, t) end;
       in (map prep ts', Ts') end;
 
diff -r e2ab4147b244 -r fa37ee54644c src/Pure/variable.ML
--- a/src/Pure/variable.ML	Tue Dec 03 22:46:24 2024 +0100
+++ b/src/Pure/variable.ML	Fri Dec 06 13:33:25 2024 +0100
@@ -326,7 +326,7 @@
     [] => t
   | bounds =>
       let
-        val names = Term.declare_term_names t (names_of ctxt);
+        val names = Term.declare_free_names t (names_of ctxt);
         val xs = rev (Name.variants names (rev (map #2 bounds)));
         fun substs (((b, T), _), x') =
           let fun subst U = (Free (b, U), Syntax_Trans.mark_bound_abs (x', U))
@@ -705,7 +705,7 @@
 
 fun focus_params bindings t ctxt =
   let
-    val ps = Term.variant_frees t (Term.strip_all_vars t);  (*as they are printed :-*)
+    val ps = Term.variant_bounds t (Term.strip_all_vars t);
     val (xs, Ts) = split_list ps;
     val (xs', ctxt') =
       (case bindings of
diff -r e2ab4147b244 -r fa37ee54644c src/Tools/induct.ML
--- a/src/Tools/induct.ML	Tue Dec 03 22:46:24 2024 +0100
+++ b/src/Tools/induct.ML	Fri Dec 06 13:33:25 2024 +0100
@@ -607,7 +607,7 @@
   let
     val maxidx = Thm.maxidx_of st;
     val goal = Thm.term_of (Thm.cprem_of st i);  (*exception Subscript*)
-    val params = Term.variant_frees goal (Logic.strip_params goal);
+    val params = Term.variant_bounds goal (Logic.strip_params goal);
   in
     if not (null params) then
       (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
diff -r e2ab4147b244 -r fa37ee54644c src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Tue Dec 03 22:46:24 2024 +0100
+++ b/src/Tools/subtyping.ML	Fri Dec 06 13:33:25 2024 +0100
@@ -244,7 +244,7 @@
     val (Ts_bTs', ts') = Type_Infer.finish ctxt tye (Ts @ map snd bs, ts);
     val (Ts', Ts'') = chop (length Ts) Ts_bTs';
     fun prep t =
-      let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
+      let val xs = rev (Term.variant_bounds t (rev (map fst bs ~~ Ts'')))
       in Term.subst_bounds (map Syntax_Trans.mark_bound_abs xs, t) end;
   in (map prep ts', Ts') end;