# HG changeset patch
# User wenzelm
# Date 1702301114 -3600
# Node ID 17fda85a33dc324dde769fd1aadcf4d1f77c6fe3
# Parent  197b155f8818765f395133efa3a8c4901da6dd07
minor performace tuning;

diff -r 197b155f8818 -r 17fda85a33dc src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Dec 11 14:05:19 2023 +0100
+++ b/src/Pure/term.ML	Mon Dec 11 14:25:14 2023 +0100
@@ -668,7 +668,7 @@
 
 fun rename_abs pat obj t =
   let
-    val renaming = match_bvs (pat, obj) [];
+    val renaming = match_bvs (pat, obj) [] |> filter_out (op =);
     fun rename x = perhaps (AList.lookup (op =) renaming) x;
   in if null renaming then NONE else Same.catch (map_abs_vars_same rename) t end;