# HG changeset patch
# User wenzelm
# Date 1702319611 -3600
# Node ID dc1681739247b5f230362e939d2469437cacd79b
# Parent  a551cf8eca09e9562f9c75a3b1707837ba42b2e3
misc tuning and clarification;

diff -r a551cf8eca09 -r dc1681739247 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Dec 11 14:26:24 2023 +0100
+++ b/src/Pure/thm.ML	Mon Dec 11 19:33:31 2023 +0100
@@ -2224,8 +2224,10 @@
 (*Use the alist to rename all bound variables and some unknowns in a term
   dpairs = current disagreement pairs;  tpairs = permanent ones (flexflex);
   Preserves unknowns in tpairs and on lhs of dpairs. *)
-fun rename_bvs [] _ _ _ _ = K I
-  | rename_bvs al dpairs tpairs B As =
+fun rename_bvs dpairs tpairs B As =
+  let val al = fold_rev Term.match_bvars dpairs [] in
+    if null al then {vars = [], bounds = []}
+    else
       let
         val add_var = fold_aterms (fn Var ((x, _), _) => Symset.insert x | _ => I);
         val unknowns =
@@ -2241,6 +2243,7 @@
              Symset.member unknowns x orelse Symset.member unknowns y)
           |> distinct (eq_fst (op =));
         val unchanged = Symset.restrict (not o AList.defined (op =) al') unknowns';
+
         fun del_clashing clash xs _ [] qs =
               if clash then del_clashing false xs xs qs [] else qs
           | del_clashing clash xs ys ((p as (x, y)) :: ps) qs =
@@ -2249,21 +2252,25 @@
               else del_clashing clash xs (Symset.insert y ys) ps (p :: qs);
         val al'' = del_clashing false unchanged unchanged al' [];
 
+      in {vars = al'', bounds = al} end
+  end;
+
+(*Function to rename bounds/unknowns in the argument, lifted over B*)
+fun rename_bvars dpairs tpairs B As =
+  let val {vars, bounds} = rename_bvs dpairs tpairs B As in
+    if null vars andalso null bounds then K I
+    else
+      let
         fun rename (t as Var ((x, i), T)) =
-              (case AList.lookup (op =) al'' x of
+              (case AList.lookup (op =) vars x of
                  SOME y => Var ((y, i), T)
                | NONE => t)
           | rename (Abs (x, T, t)) =
-              Abs (perhaps (AList.lookup (op =) al) x, T, rename t)
+              Abs (perhaps (AList.lookup (op =) bounds) x, T, rename t)
           | rename (f $ t) = rename f $ rename t
           | rename t = t;
-        fun strip_ren f Ai = f rename B Ai
-      in strip_ren end;
-
-(*Function to rename bounds/unknowns in the argument, lifted over B*)
-fun rename_bvars dpairs =
-  rename_bvs (fold_rev Term.match_bvars dpairs []) dpairs;
-
+      in fn apply => fn t => apply rename B t end
+  end;
 
 
 (*** RESOLUTION ***)