# HG changeset patch
# User wenzelm
# Date 1672237537 -3600
# Node ID ad01b550e74b3dfc4de7902b34aae0bcb09783df
# Parent  f425e0fda79c3f601b165b825325267308bac4e5
tuned;

diff -r f425e0fda79c -r ad01b550e74b src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML	Wed Dec 28 14:52:03 2022 +0100
+++ b/src/Pure/Tools/generated_files.ML	Wed Dec 28 15:25:37 2022 +0100
@@ -285,10 +285,9 @@
 fun check_external_files ctxt (raw_files, raw_base_dir) =
   let
     val base_dir = Resources.check_dir ctxt NONE raw_base_dir;
-    fun check source =
+    val files = raw_files |> map (fn source =>
      (Resources.check_file ctxt (SOME base_dir) source;
-      Path.explode (Input.string_of source));
-    val files = map check raw_files;
+      Path.explode (Input.string_of source)));
   in (files, base_dir) end;
 
 fun get_external_files dir (files, base_dir) =