src/Pure/Thy/sessions.scala
changeset 65999 ee4cf96a9406
parent 65938 1b297ce1e8aa
child 66195 bb886f13623a
--- a/src/Pure/Thy/sessions.scala	Thu Jun 01 21:24:33 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Jun 01 21:43:36 2017 +0200
@@ -574,7 +574,7 @@
           val global_theories =
             for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }
             yield {
-              val thy_name = Path.explode(thy).expand.base.implode
+              val thy_name = Path.explode(thy).expand.base_name
               if (Long_Name.is_qualified(thy_name))
                 error("Bad qualified name for global theory " +
                   quote(thy_name) + Position.here(pos))