# HG changeset patch
# User wenzelm
# Date 1633168571 -7200
# Node ID 71dfb835025d60a04e7b6dcbea3f63cf5e91cd9f
# Parent  ed4149b3d7ab835ea8d1cdfefe27bb96fcd93457
tuned, following Syntax_Trans.variant_abs;

diff -r ed4149b3d7ab -r 71dfb835025d src/Pure/term.ML
--- a/src/Pure/term.ML	Sat Oct 02 11:38:39 2021 +0200
+++ b/src/Pure/term.ML	Sat Oct 02 11:56:11 2021 +0200
@@ -964,17 +964,19 @@
 
 (* dest abstraction *)
 
-fun dest_abs (x, T, body) =
+fun used_free x =
   let
-    fun name_clash (Free (y, _)) = (x = y)
-      | name_clash (t $ u) = name_clash t orelse name_clash u
-      | name_clash (Abs (_, _, t)) = name_clash t
-      | name_clash _ = false;
-  in
-    if name_clash body then
-      dest_abs (singleton (Name.variant_list [x]) x, T, body)    (*potentially slow*)
-    else (x, subst_bound (Free (x, T), body))
-  end;
+    fun used (Free (y, _)) = (x = y)
+      | used (t $ u) = used t orelse used u
+      | used (Abs (_, _, t)) = used t
+      | used _ = false;
+  in used end;
+
+fun dest_abs (x, T, b) =
+  if used_free x b then
+    let val (x', _) = Name.variant x (declare_term_names b Name.context)
+    in (x', subst_bound (Free (x', T), b)) end
+  else (x, subst_bound (Free (x, T), b));
 
 
 (* dummy patterns *)