clarified Term.dest_abs (again, refining 71dfb835025d): only Free names are relevant for abstract terms, without syntax;

--- a/src/Pure/term.ML	Sat Oct 02 12:15:37 2021 +0200
+++ b/src/Pure/term.ML	Sat Oct 02 12:45:51 2021 +0200
@@ -974,7 +974,7 @@
 
 fun dest_abs (x, T, b) =
   if used_free x b then
-    let val (x', _) = Name.variant x (declare_term_names b Name.context)
+    let val (x', _) = Name.variant x (declare_term_frees b Name.context);
     in (x', subst_bound (Free (x', T), b)) end
   else (x, subst_bound (Free (x, T), b));