diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 8a86e1974b..eda3db1b3c 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -335,9 +335,9 @@ def elabMutual : CommandElab := fun stx => do
       `($[unsafe%$unsafe?]? def initFn : IO $type := with_decl_name% ?$id do $doSeq
         $[$doc?:docComment]? @[$attrId:ident initFn, $(attrs?.getD ∅),*] $(vis?)? opaque $id : $type)
     else
-      let `(Parser.Command.declModifiersT| ) := declModifiers
+      let `(Parser.Command.declModifiersT| $[$doc?:docComment]? ) := declModifiers
         | Macro.throwErrorAt declModifiers "invalid initialization command, unexpected modifiers"
-      `(@[$attrId:ident] def initFn : IO Unit := do $doSeq)
+      `($[$doc?:docComment]? @[$attrId:ident] def initFn : IO Unit := do $doSeq)
   | _ => Macro.throwUnsupported
 
 builtin_initialize