src/Doc/Implementation/Logic.thy

 
 
   \<^rail>\<open>
     @{syntax_def type_const}: @{syntax name} (@{syntax embedded_ml}*)
     ;
-    @{syntax_def type_const_fn}: @{syntax type_const} @'=>' @{syntax embedded}
+    @{syntax_def type_const_fn}: @{syntax type_const} @'=>' @{syntax embedded_ml}
     ;
-    @{syntax_def embedded_ml}: @{syntax embedded} |
-      @{syntax control_symbol} @{syntax embedded} | @'_'
+    @{syntax_def embedded_ml}:
+      @'_' | @{syntax embedded} | @{syntax control_symbol} @{syntax embedded}
   \<close>
 
   The text provided as @{syntax embedded_ml} is treated as regular Isabelle/ML
   source, possibly with nested antiquotations. ML text that only consists of a
   single antiquotation in compact control-cartouche notation, can be written

 
   \<^rail>\<open>
     @{syntax_def term_const}:
       @{syntax name} (@{syntax embedded_ml}*) (@{syntax for_args})?
     ;
-    @{syntax_def term_const_fn}: @{ syntax term_const} @'=>' @{syntax embedded}
+    @{syntax_def term_const_fn}:
+      @{syntax term_const} @'=>' @{syntax embedded_ml}
     ;
-    @{syntax_def for_args}: @'for' (@{syntax embedded_ml}*)
+    @{syntax_def for_args}: @'for' (@{syntax embedded_ml}+)
   \<close>
 \<close>
 
 text %mlex \<open>
   Here are some minimal examples for term constant antiquotations. Type