changeset 69366 | b6dacf6eabe3 |
parent 69349 | 7cef9e386ffe |
child 69876 | b49bd228ac8a |
--- a/src/Pure/Thy/thy_header.ML Wed Nov 28 15:38:18 2018 +0100 +++ b/src/Pure/Thy/thy_header.ML Wed Nov 28 16:14:31 2018 +0100 @@ -121,7 +121,7 @@ fun import_name s = if String.isSuffix ".thy" s then error ("Malformed theory import: " ^ quote s) - else Path.base_name (Path.explode s); + else Path.file_name (Path.explode s); (* header args *)