# HG changeset patch
# User wenzelm
# Date 1732983270 -3600
# Node ID 44c0028486db0f003d5bc871ef79b61696e312e3
# Parent  98cb63b447c6814efafa21d42b31db610e9bb6aa
tuned signature: more operations;

diff -r 98cb63b447c6 -r 44c0028486db src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sat Nov 30 16:42:22 2024 +0100
+++ b/src/Pure/more_thm.ML	Sat Nov 30 17:14:30 2024 +0100
@@ -353,8 +353,7 @@
 
 fun used_vars i =
   Name.build_context o
-    (Thm.fold_terms {hyps = false} o Term.fold_aterms)
-      (fn Var ((x, j), _) => i = j ? Name.declare x | _ => I);
+    Thm.fold_terms {hyps = false} (Term.declare_var_names (fn j => i = j));
 
 fun dest_all ct used =
   (case Thm.term_of ct of
diff -r 98cb63b447c6 -r 44c0028486db src/Pure/term.ML
--- a/src/Pure/term.ML	Sat Nov 30 16:42:22 2024 +0100
+++ b/src/Pure/term.ML	Sat Nov 30 17:14:30 2024 +0100
@@ -153,7 +153,10 @@
   val add_consts: term -> (string * typ) list -> (string * typ) list
   val declare_tfree_namesT: typ -> Name.context -> Name.context
   val declare_tfree_names: term -> Name.context -> Name.context
+  val declare_tvar_namesT: (int -> bool) -> typ -> Name.context -> Name.context
+  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 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
@@ -576,7 +579,10 @@
 val add_consts = fold_aterms (fn Const c => insert (op =) c | _ => I);
 val declare_tfree_namesT = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
 val declare_tfree_names = fold_types declare_tfree_namesT;
+fun declare_tvar_namesT pred = fold_atyps (fn TVar ((a, i), _) => pred i ? Name.declare a | _ => I);
+val declare_tvar_names = fold_types o declare_tvar_namesT;
 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);
 
 (*extra type variables in a term, not covered by its type*)
 fun hidden_polymorphism t =
diff -r 98cb63b447c6 -r 44c0028486db src/Pure/type.ML
--- a/src/Pure/type.ML	Sat Nov 30 16:42:22 2024 +0100
+++ b/src/Pure/type.ML	Sat Nov 30 17:14:30 2024 +0100
@@ -345,9 +345,7 @@
     val xs =
       build (t |> (Term.fold_types o Term.fold_atyps)
         (fn TFree v => if TFrees.defined fixed v then I else insert (op =) v | _ => I));
-    val used =
-      Name.build_context (t |>
-        (fold_types o fold_atyps) (fn TVar ((a, _), _) => Name.declare a | _ => I));
+    val used = Name.build_context (t |> Term.declare_tvar_names (K true));
     val ys = #1 (fold_map Name.variant (map #1 xs) used);
   in map2 (fn (a, S) => fn b => ((a, S), ((b, 0), S))) xs ys end;
 
diff -r 98cb63b447c6 -r 44c0028486db src/Tools/IsaPlanner/isand.ML
--- a/src/Tools/IsaPlanner/isand.ML	Sat Nov 30 16:42:22 2024 +0100
+++ b/src/Tools/IsaPlanner/isand.ML	Sat Nov 30 17:14:30 2024 +0100
@@ -56,10 +56,7 @@
   let
     val names =
       Variable.names_of ctxt
-      |> (fold o fold_aterms)
-          (fn Var ((a, _), _) => Name.declare a
-            | Free (a, _) => Name.declare a
-            | _ => I) ts;
+      |> fold (fn t => Term.declare_free_names t #> Term.declare_var_names (K true) t) ts;
   in fst (fold_map Name.variant xs names) end;
 
 (* fix parameters of a subgoal "i", as free variables, and create an