# HG changeset patch
# User wenzelm
# Date 1425215749 -3600
# Node ID 7e4bf0824cd363efe7aee7748d16359c61dc5890
# Parent  1081f91c0662b029b6cd877972631a182a4d3d7d
tuned;

diff -r 1081f91c0662 -r 7e4bf0824cd3 src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Sat Feb 28 21:51:34 2015 +0100
+++ b/src/Doc/Implementation/ML.thy	Sun Mar 01 14:15:49 2015 +0100
@@ -1116,7 +1116,7 @@
 
   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