--- 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>