--- a/src/Pure/Thy/thy_header.ML Fri Oct 06 17:13:57 2017 +0200
+++ b/src/Pure/Thy/thy_header.ML Fri Oct 06 21:14:00 2017 +0200
@@ -20,6 +20,7 @@
val ml_bootstrapN: string
val ml_roots: string list
val bootstrap_thys: string list
+ val is_base_name: string -> bool
val import_name: string -> string
val args: header parser
val read: Position.T -> string -> header
@@ -114,6 +115,9 @@
val ml_roots = ["ML_Root0", "ML_Root"];
val bootstrap_thys = ["Bootstrap_Pure", "Bootstrap_ML_Bootstrap"];
+fun is_base_name s =
+ s <> "" andalso not (exists_string (member (op =) ["/", "\\", ":"]) s)
+
val import_name = Path.base_name o Path.explode;