src/Doc/Implementation/ML.thy

   exception state, the system will print the result on the error
   channel (see \secref{sec:message-channels}).
 
   It is considered bad style to refer to internal function names or
   values in ML source notation in user error messages.  Do not use
-  @{text "@{make_string}"} here!
+  @{text "@{make_string}"} nor @{text "@{here}"}!
 
   Grammatical correctness of error messages can be improved by
   \emph{omitting} final punctuation: messages are often concatenated
   or put into a larger context (e.g.\ augmented with source position).
   Note that punctuation after formal entities (types, terms, theorems) is