src/Doc/Implementation/Logic.thy

   @{ML_antiquotation_def "nonterminal"} & : & \<open>ML_antiquotation\<close> \\
   @{ML_antiquotation_def "typ"} & : & \<open>ML_antiquotation\<close> \\
   \end{matharray}
 
   @{rail \<open>
-  @@{ML_antiquotation class} nameref
+  @@{ML_antiquotation class} name
   ;
   @@{ML_antiquotation sort} sort
   ;
   (@@{ML_antiquotation type_name} |
    @@{ML_antiquotation type_abbrev} |
-   @@{ML_antiquotation nonterminal}) nameref
+   @@{ML_antiquotation nonterminal}) name
   ;
   @@{ML_antiquotation typ} type
   \<close>}
 
   \<^descr> \<open>@{class c}\<close> inlines the internalized class \<open>c\<close> --- as @{ML_type string}

   @{ML_antiquotation_def "prop"} & : & \<open>ML_antiquotation\<close> \\
   \end{matharray}
 
   @{rail \<open>
   (@@{ML_antiquotation const_name} |
-   @@{ML_antiquotation const_abbrev}) nameref
+   @@{ML_antiquotation const_abbrev}) name
   ;
   @@{ML_antiquotation const} ('(' (type + ',') ')')?
   ;
   @@{ML_antiquotation term} term
   ;

   ;
   @@{ML_antiquotation cterm} term
   ;
   @@{ML_antiquotation cprop} prop
   ;
-  @@{ML_antiquotation thm} thmref
+  @@{ML_antiquotation thm} thm
   ;
-  @@{ML_antiquotation thms} thmrefs
+  @@{ML_antiquotation thms} thms
   ;
   @@{ML_antiquotation lemma} ('(' @'open' ')')? ((prop +) + @'and') \<newline>
     @'by' method method?
   \<close>}