diff -r 4e4738698db4 -r 9f394a16c557 src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Doc/Implementation/ML.thy	Wed Apr 13 18:01:05 2016 +0200
@@ -653,10 +653,10 @@
   special syntactic entities of the following form:
 
   @{rail \<open>
-  @{syntax_def antiquote}: '@{' nameref args '}'
+  @{syntax_def antiquote}: '@{' name args '}'
   \<close>}
 
-  Here @{syntax nameref} and @{syntax args} are outer syntax categories, as
+  Here @{syntax name} and @{syntax args} are outer syntax categories, as
   defined in @{cite "isabelle-isar-ref"}.
 
   \<^medskip>