src/Doc/Isar_Ref/HOL_Specific.thy

     @{command_def (HOL) "code_reflect"} & : & \<open>theory \<rightarrow> theory\<close> \\
     @{command_def (HOL) "code_pred"} & : & \<open>theory \<rightarrow> proof(prove)\<close>
   \end{matharray}
 
   \<^rail>\<open>
-    @@{command (HOL) export_code} @'open'? (const_expr+) \<newline>
-       ((@'in' target (@'module_name' @{syntax string})? \<newline>
-        (@'file' @{syntax string})? ('(' args ')')?)+) ?
+    @@{command (HOL) export_code} @'open'? \<newline> (const_expr+) (export_target*)
+    ;
+    export_target:
+      @'in' target (@'module_name' @{syntax string})? \<newline>
+      (@'file' @{syntax string})? ('(' args ')')?
+    ;
+    target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
+    ;
+    const_expr: (const | 'name._' | '_')
     ;
     const: @{syntax term}
     ;
-    const_expr: (const | 'name._' | '_')
-    ;
     type_constructor: @{syntax name}
     ;
     class: @{syntax name}
-    ;
-    target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
     ;
     @@{attribute (HOL) code} ('equation' | 'nbe' | 'abstype' | 'abstract'
       | 'del' | 'drop:' (const+) | 'abort:' (const+))?
     ;
     @@{command (HOL) code_datatype} (const+)