# HG changeset patch
# User wenzelm
# Date 1702319788 -3600
# Node ID 288229384ed7943402b3e4a6041b5d46546da5dd
# Parent  dc1681739247b5f230362e939d2469437cacd79b
revert 17fda85a33dc: renaming is not necessarily unique, e.g. [("x", "x"), ("x", "y")];

diff -r dc1681739247 -r 288229384ed7 src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Dec 11 19:33:31 2023 +0100
+++ b/src/Pure/term.ML	Mon Dec 11 19:36:28 2023 +0100
@@ -668,7 +668,7 @@
 
 fun rename_abs pat obj t =
   let
-    val renaming = match_bvs (pat, obj) [] |> filter_out (op =);
+    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;