[Isabelle] "test" as an identifier leads to surprising errors

[wimmers]

Problem description:
If "test" is used in Submission.thy we get surprising errors.

Example (Submission.thy):

...

lemma test: True
 by simp

...

Output:

...
Draft.Submission | Outer syntax error\<^here>: proposition expected, but end-of-input\<^here> was found
-- | --
Draft.Submission | Outer syntax error\<^here>: term expected, but keyword :\<^here> was found
Draft.Submission | Bad context for command "apply"\<^here> -- using reset state
...

Expected behavior: The system should accept the submission.

Analysis:
In OK_Test.thy, we define the command test and thus reserve it as a keyword.

Solution proposals:

• Warn user if "test" is used as an identifier
• Find a less common name, and hope it will not be used
• Find a way to register the command in the proper context but to bind the command only later. This would also be the preferred solution for other commands defined in OK_Test.thy.