NEWS

 unconditional, with ln_mult_pos and ln_divide_pos introduced for legacy
 purposes.
 
 
 *** 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,
 bottom-up, top-down etc. until a normal form is reached. This often