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.
tuned comments (see also 476a239d3e0e and possibly 4b62e0cb3aa8);
authorwenzelm
Mon, 11 Dec 2023 22:08:43 +0100
changeset 79256 4a97f2daf2c0
parent 79255 2b2e51cc5c70
child 79257 d33ec0c3672e
tuned comments (see also 476a239d3e0e and possibly 4b62e0cb3aa8);
src/Pure/thm.ML file | annotate | diff | comparison | revisions 
--- 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 =
isabelle