# HG changeset patch
# User wenzelm
# Date 1702328923 -3600
# Node ID 4a97f2daf2c0fb6355016a1308876f3e31e81e03
# Parent  2b2e51cc5c700ff74b5f533553f9d15ea16f963e
tuned comments (see also 476a239d3e0e and possibly 4b62e0cb3aa8);

diff -r 2b2e51cc5c70 -r 4a97f2daf2c0 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 =