diff -r 5efaa884ac6c -r 256fc20716f2 src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Aug 11 18:26:16 2016 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Aug 11 18:26:44 2016 +0200
@@ -195,8 +195,9 @@
       @@{antiquotation emph} options @{syntax text} |
       @@{antiquotation bold} options @{syntax text} |
       @@{antiquotation verbatim} options @{syntax text} |
+      @@{antiquotation path} options @{syntax name} |
       @@{antiquotation "file"} options @{syntax name} |
-      @@{antiquotation file_unchecked} options @{syntax name} |
+      @@{antiquotation dir} options @{syntax name} |
       @@{antiquotation url} options @{syntax embedded} |
       @@{antiquotation cite} options @{syntax cartouche}? (@{syntax name} + @'and')
     ;
@@ -283,11 +284,13 @@
   \<^descr> \<open>@{verbatim s}\<close> prints uninterpreted source text literally as ASCII
   characters, using some type-writer font style.
 
-  \<^descr> \<open>@{file path}\<close> checks that \<open>path\<close> refers to a file (or directory) and
-  prints it verbatim.
+  \<^descr> \<open>@{path name}\<close> prints the file-system path name verbatim.
 
-  \<^descr> \<open>@{file_unchecked path}\<close> is like \<open>@{file path}\<close>, but does not check the
-  existence of the \<open>path\<close> within the file-system.
+  \<^descr> \<open>@{file name}\<close> is like \<open>@{path name}\<close>, but ensures that \<open>name\<close> refers to a
+  plain file.
+
+  \<^descr> \<open>@{dir name}\<close> is like \<open>@{path name}\<close>, but ensures that \<open>name\<close> refers to a
+  directory.
 
   \<^descr> \<open>@{url name}\<close> produces markup for the given URL, which results in an
   active hyperlink within the text.