clarified: 'imports' is de-facto mandatory;

--- a/src/Doc/Isar_Ref/Spec.thy	Tue Aug 02 17:35:18 2016 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Tue Aug 02 17:39:38 2016 +0200
@@ -58,9 +58,8 @@
   such a global @{command (global) "end"}.
 
   @{rail \<open>
-    @@{command theory} @{syntax name} imports? \<newline> keywords? abbrevs? @'begin'
-    ;
-    imports: @'imports' (@{syntax name} +)
+    @@{command theory} @{syntax name} @'imports' (@{syntax name} +) \<newline>
+      keywords? abbrevs? @'begin'
     ;
     keywords: @'keywords' (keyword_decls + @'and')
     ;