Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
minor performance tuning;
authorwenzelm
Mon, 11 Dec 2023 20:17:13 +0100
changeset 79250 1414443e11c6
parent 79249 718798653cf1
child 79251 a32428d81fe5
minor performance tuning;
src/Pure/term.ML file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle