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