diff -r eb4f59275c05 -r 5a7c919a4ada src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Aug 12 11:54:36 2016 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Aug 12 13:16:04 2016 +0200
@@ -195,7 +195,7 @@
       @@{antiquotation emph} options @{syntax text} |
       @@{antiquotation bold} options @{syntax text} |
       @@{antiquotation verbatim} options @{syntax text} |
-      @@{antiquotation path} options @{syntax name} |
+      @@{antiquotation path} options @{syntax embedded} |
       @@{antiquotation "file"} options @{syntax name} |
       @@{antiquotation dir} options @{syntax name} |
       @@{antiquotation url} options @{syntax embedded} |