# HG changeset patch
# User wenzelm
# Date 1733262384 -3600
# Node ID e2ab4147b244b50d1a4ba2f4dd89ce1378dadf25
# Parent  5335b1ca6233d74aadeb8aad60ee4cbbc39b476f
prefer Term.variant_bounds: bounds vs. frees, no attempt at consts;

diff -r 5335b1ca6233 -r e2ab4147b244 NEWS
--- a/NEWS	Mon Dec 02 22:16:29 2024 +0100
+++ b/NEWS	Tue Dec 03 22:46:24 2024 +0100
@@ -241,6 +241,17 @@
 
 *** ML ***
 
+* Term.variant_bounds replaces former Term.variant_frees for logical
+manipulation of terms, without inner-syntax operations (e.g. reading a
+term in the context of goal parameters). In contrast, former
+Term.variant_frees made some attempts to work with constants as well,
+but without taking the formal name space or abbreviations into account.
+The existing operations Logic.goal_params, Logic.concl_of_goal,
+Logic.prems_of_goal are now based on Term.variant_bounds, and thus
+change their semantics silently! Rare INCOMPATIBILITY, better use
+Variable.variant_names or Variable.focus_params, instead of
+Logic.goal_params etc.
+
 * Antiquotation \<^bundle>\<open>name\<close> inlines a formally checked bundle name.
 
 * The new operation Pattern.rewrite_term_yoyo alternates top-down,
diff -r 5335b1ca6233 -r e2ab4147b244 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Mon Dec 02 22:16:29 2024 +0100
+++ b/src/Pure/logic.ML	Tue Dec 03 22:46:24 2024 +0100
@@ -667,7 +667,7 @@
 (*reverses parameters for substitution*)
 fun goal_params st i =
   let val gi = get_goal st i
-      val rfrees = map Free (rev (Term.variant_frees gi (strip_params gi)))
+      val rfrees = map Free (rev (Term.variant_bounds gi (strip_params gi)))
   in (gi, rfrees) end;
 
 fun concl_of_goal st i =