# HG changeset patch
# User wenzelm
# Date 1672232880 -3600
# Node ID 6e786a09a4bbb8101c5c673c8dff0cc9a662fe07
# Parent  69d8d16c56124412da859486a4cb0e337cee2e1a
tuned;

diff -r 69d8d16c5612 -r 6e786a09a4bb src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Wed Dec 28 12:30:18 2022 +0100
+++ b/src/Pure/PIDE/resources.ML	Wed Dec 28 14:08:00 2022 +0100
@@ -360,7 +360,7 @@
   parse_files make_paths >> (fn files => fn thy =>
     let
       val fs = files thy;
-      val thy' = fold (fn {src_path, digest, ...} => provide (src_path, digest)) fs thy;
+      val thy' = fold provide_file fs thy;
     in (fs, thy') end);
 
 val provide_parse_file = provide_parse_files single >> (fn f => f #>> the_single);