src/Doc/Isar_Ref/Document_Preparation.thy

   @{rail \<open>
     @{syntax_def antiquotation_body}:
       (@@{antiquotation text} | @@{antiquotation cartouche} | @@{antiquotation theory_text})
         options @{syntax text} |
       @@{antiquotation theory} options @{syntax name} |
-      @@{antiquotation thm} options styles @{syntax thmrefs} |
+      @@{antiquotation thm} options styles @{syntax thms} |
       @@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
       @@{antiquotation prop} options styles @{syntax prop} |
       @@{antiquotation term} options styles @{syntax term} |
       @@{antiquotation (HOL) value} options styles @{syntax term} |
       @@{antiquotation term_type} options styles @{syntax term} |

         options @{syntax name}
     ;
     @{syntax antiquotation}:
       @@{antiquotation goals} options |
       @@{antiquotation subgoals} options |
-      @@{antiquotation prf} options @{syntax thmrefs} |
-      @@{antiquotation full_prf} options @{syntax thmrefs} |
+      @@{antiquotation prf} options @{syntax thms} |
+      @@{antiquotation full_prf} options @{syntax thms} |
       @@{antiquotation ML} options @{syntax text} |
       @@{antiquotation ML_op} options @{syntax text} |
       @@{antiquotation ML_type} options @{syntax text} |
       @@{antiquotation ML_structure} options @{syntax text} |
       @@{antiquotation ML_functor} options @{syntax text} |
       @@{antiquotation emph} options @{syntax text} |
       @@{antiquotation bold} options @{syntax text} |
       @@{antiquotation verbatim} options @{syntax text} |
-      @@{antiquotation "file"} options @{syntax xname} |
-      @@{antiquotation file_unchecked} options @{syntax xname} |
+      @@{antiquotation "file"} options @{syntax name} |
+      @@{antiquotation file_unchecked} options @{syntax name} |
       @@{antiquotation url} options @{syntax name} |
       @@{antiquotation cite} options @{syntax cartouche}? (@{syntax name} + @'and')
     ;
     styles: '(' (style + ',') ')'
     ;

   \begin{matharray}{rcl}
     @{command_def "display_drafts"}\<open>\<^sup>*\<close> & : & \<open>any \<rightarrow>\<close> \\
   \end{matharray}
 
   @{rail \<open>
-    @@{command display_drafts} (@{syntax xname} +)
+    @@{command display_drafts} (@{syntax name} +)
   \<close>}
 
   \<^descr> @{command "display_drafts"}~\<open>paths\<close> performs simple output of a given list
   of raw source files. Only those symbols that do not require additional
   {\LaTeX} packages are displayed properly, everything else is left verbatim.