diff -r e74444bdd310 -r f12a52b5d812 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Mar 28 12:59:44 2019 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Mar 28 13:06:32 2019 +0100
@@ -2281,20 +2281,22 @@
   \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+))?
     ;