src/Pure/thm.ML

--- a/src/Pure/thm.ML	Mon Dec 11 21:56:24 2023 +0100
+++ b/src/Pure/thm.ML	Mon Dec 11 22:08:43 2023 +0100
@@ -2244,6 +2244,7 @@
           |> distinct (eq_fst (op =));
         val unchanged = Symset.restrict (not o AList.defined (op =) al') unknowns';
 
+        (*avoid introducing name clashes between schematic variables*)
         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 =