src/Doc/Isar_Ref/Inner_Syntax.thy

     ;
     @@{command term} @{syntax modes}? @{syntax term}
     ;
     @@{command prop} @{syntax modes}? @{syntax prop}
     ;
-    @@{command thm} @{syntax modes}? @{syntax thmrefs}
-    ;
-    ( @@{command prf} | @@{command full_prf} ) @{syntax modes}? @{syntax thmrefs}?
+    @@{command thm} @{syntax modes}? @{syntax thms}
+    ;
+    ( @@{command prf} | @@{command full_prf} ) @{syntax modes}? @{syntax thms}?
     ;
     @@{command print_state} @{syntax modes}?
     ;
     @{syntax_def modes}: '(' (@{syntax name} + ) ')'
   \<close>}

   for explicit notation. This allows to add or delete mixfix annotations for
   of existing logical entities within the current context.
 
   @{rail \<open>
     (@@{command type_notation} | @@{command no_type_notation}) @{syntax mode}? \<newline>
-      (@{syntax nameref} @{syntax mixfix} + @'and')
+      (@{syntax name} @{syntax mixfix} + @'and')
     ;
     (@@{command notation} | @@{command no_notation}) @{syntax mode}? \<newline>
-      (@{syntax nameref} @{syntax mixfix} + @'and')
-    ;
-    @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax mixfix} + @'and')
+      (@{syntax name} @{syntax mixfix} + @'and')
+    ;
+    @@{command write} @{syntax mode}? (@{syntax name} @{syntax mixfix} + @'and')
   \<close>}
 
   \<^descr> @{command "type_notation"}~\<open>c (mx)\<close> associates mixfix syntax with an
   existing type constructor. The arity of the constructor is retrieved from
   the context.

 
     constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}?
     ;
     mode: ('(' ( @{syntax name} | @'output' | @{syntax name} @'output' ) ')')
     ;
-    transpat: ('(' @{syntax nameref} ')')? @{syntax string}
+    transpat: ('(' @{syntax name} ')')? @{syntax string}
   \<close>}
 
   \<^descr> @{command "nonterminal"}~\<open>c\<close> declares a type constructor \<open>c\<close> (without
   arguments) to act as purely syntactic type: a nonterminal symbol of the
   inner syntax.