diff -r 5900b58d6bd4 -r 4329a8fecbe1 src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML	Fri Jan 17 11:16:11 2025 +0100
+++ b/src/Pure/Tools/generated_files.ML	Fri Jan 17 11:24:40 2025 +0100
@@ -253,7 +253,7 @@
 
     val (path, pos) = Path.dest_binding binding;
     val file_type =
-      get_file_type thy (#2 (Path.split_ext path))
+      get_file_type thy (Path.get_ext path)
         handle ERROR msg => error (msg ^ Position.here pos);
 
     val header = #make_comment file_type " generated by Isabelle ";