more robust, for the sake of very rare duplicate files: src/Doc/Prog_Prove/MyList.thy and $AFP/Case_Labeling/util.ML;
--- 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
}