diff -r 122df1fde073 -r 925d10a7a610 src/Pure/Thy/thy_header.ML
--- 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;