changeset 81843 | 4329a8fecbe1 |
parent 81842 | 5900b58d6bd4 |
--- 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 ";