
diff -r d0c1b2dbca5b -r 5bf08c9aa036 src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Wed Apr 13 11:26:52 2016 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Wed Apr 13 11:31:13 2016 +0200
@@ -195,8 +195,8 @@
       @@{antiquotation emph} options @{syntax text} |
       @@{antiquotation bold} options @{syntax text} |
       @@{antiquotation verbatim} options @{syntax text} |
-      @@{antiquotation "file"} options @{syntax name} |
-      @@{antiquotation file_unchecked} options @{syntax name} |
+      @@{antiquotation "file"} options @{syntax xname} |
+      @@{antiquotation file_unchecked} options @{syntax xname} |
       @@{antiquotation url} options @{syntax name} |
       @@{antiquotation cite} options @{syntax cartouche}? (@{syntax name} + @'and')
     ;
@@ -613,7 +613,7 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command display_drafts} (@{syntax name} +)
+    @@{command display_drafts} (@{syntax xname} +)
   \<close>}
 
   \<^descr> @{command "display_drafts"}~\<open>paths\<close> performs simple output of a given list




