# HG changeset patch
# User wenzelm
# Date 1633171551 -7200
# Node ID 254de9de2cd7fde417eacc50d9eb7794a1f3135e
# Parent  83d2208252d1e0c3f21c7a968f1353b0922b1eaf
clarified Term.dest_abs (again, refining 71dfb835025d): only Free names are relevant for abstract terms, without syntax;

diff -r 83d2208252d1 -r 254de9de2cd7 src/Pure/term.ML
--- 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));