uniform system name;

--- a/src/Pure/Isar/parse.scala	Tue Oct 24 21:20:55 2017 +0200
+++ b/src/Pure/Isar/parse.scala	Wed Oct 25 11:35:48 2017 +0200
@@ -72,8 +72,8 @@
     def path: Parser[String] =
       atom("file name/path specification", tok => tok.is_embedded && Path.is_wellformed(tok.content))
 
-    def theory_name: Parser[String] =
-      atom("theory name", tok => tok.is_name && Path.is_wellformed(tok.content))
+    def session_name: Parser[String] = atom("session name", _.is_system_name)
+    def theory_name: Parser[String] = atom("theory name", _.is_system_name)
 
     private def tag_name: Parser[String] =
       atom("tag name", tok =>

--- a/src/Pure/Isar/token.scala	Tue Oct 24 21:20:55 2017 +0200
+++ b/src/Pure/Isar/token.scala	Wed Oct 25 11:35:48 2017 +0200
@@ -305,4 +305,6 @@
     else if (kind == Token.Kind.CARTOUCHE) Scan.Parsers.cartouche_content(source)
     else if (kind == Token.Kind.COMMENT) Scan.Parsers.comment_content(source)
     else source
+
+  def is_system_name: Boolean = is_name && Path.is_wellformed(content)
 }

--- a/src/Pure/Thy/sessions.scala	Tue Oct 24 21:20:55 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Oct 25 11:35:48 2017 +0200
@@ -582,8 +582,6 @@
 
     private val session_entry: Parser[Session_Entry] =
     {
-      val session_name = atom("session name", _.is_name)
-
       val option =
         option_name ~ opt($$$("=") ~! option_value ^^
           { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }