# HG changeset patch
# User wenzelm
# Date 1672606905 -3600
# Node ID 90c552d28d360c1888d77ffeab956fb858ee746e
# Parent  5efc770dd727b5c25526ab5b00d1cf5feb952c6f
more robust, for the sake of very rare duplicate files: src/Doc/Prog_Prove/MyList.thy and $AFP/Case_Labeling/util.ML;

diff -r 5efc770dd727 -r 90c552d28d36 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun Jan 01 21:44:08 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Sun Jan 01 22:01:45 2023 +0100
@@ -249,7 +249,7 @@
     var cache_sources = Map.empty[JFile, SHA1.Digest]
     def check_sources(paths: List[Path]): List[(Path, SHA1.Digest)] = {
       for {
-        path <- paths
+        path <- Library.distinct(paths)
         file = path.file
         if cache_sources.isDefinedAt(file) || file.isFile
       }