# HG changeset patch
# User wenzelm
# Date 1702322233 -3600
# Node ID 1414443e11c6001c57c0f8baaa3ef9bb6af83f26
# Parent  718798653cf1819b0c361bc480dc725064aac415
minor performance tuning;

diff -r 718798653cf1 -r 1414443e11c6 src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Dec 11 19:51:30 2023 +0100
+++ b/src/Pure/term.ML	Mon Dec 11 20:17:13 2023 +0100
@@ -668,9 +668,9 @@
 
 fun rename_abs pat obj t =
   let
-    val renaming = match_bvs (pat, obj) [];
-    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;
+    val renaming = Symtab.make_distinct (match_bvs (pat, obj) []);
+    fun rename x = perhaps (Symtab.lookup renaming) x;
+  in if Symtab.forall (op =) renaming then NONE else Same.catch (map_abs_vars_same rename) t end;
 
 (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
    (Bound 0) is loose at level 0 *)