changeset 72857 | a9e091ccd450 |
parent 72853 | d0038b553e0e |
child 73359 | d8a0e996614b |
--- a/src/Pure/Thy/thy_header.scala Wed Dec 09 15:14:24 2020 +0100 +++ b/src/Pure/Thy/thy_header.scala Wed Dec 09 15:53:45 2020 +0100 @@ -90,12 +90,6 @@ case _ => None } - def dir_name(s: String): String = - split_file_name(s) match { - case Some((dir, _)) => dir - case None => "" - } - def import_name(s: String): String = s match { case File_Name(name) if !name.endsWith(".thy") => name