diff -r 6d092a5166f1 -r ac979f750c1a src/Pure/Isar/parse.scala --- a/src/Pure/Isar/parse.scala Mon Mar 03 11:37:06 2014 +0100 +++ b/src/Pure/Isar/parse.scala Mon Mar 03 11:58:07 2014 +0100 @@ -62,9 +62,9 @@ def ML_source: Parser[String] = atom("ML source", _.is_text) def document_source: Parser[String] = atom("document source", _.is_text) def path: Parser[String] = - atom("file name/path specification", tok => tok.is_name && Path.is_ok(tok.content)) + atom("file name/path specification", tok => tok.is_name && Path.is_wellformed(tok.content)) def theory_name: Parser[String] = - atom("theory name", tok => tok.is_name && Thy_Load.is_ok(tok.content)) + atom("theory name", tok => tok.is_name && Thy_Load.is_wellformed(tok.content)) private def tag_name: Parser[String] = atom("tag name", tok =>