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))