diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 08ca210182..afe1a87950 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -332,14 +332,12 @@ def elabMutual : CommandElab := fun stx => do
     if let (some id, some type) := (id?, type?) then
       let `(Parser.Command.declModifiersT| $[$doc?:docComment]? $[@[$attrs?,*]]? $(vis?)? $[unsafe%$unsafe?]?) := stx[0]
         | Macro.throwErrorAt declModifiers "invalid initialization command, unexpected modifiers"
-      let declModifiers ← `(Parser.Command.declModifiersT| $[$doc?:docComment]? @[$attrId:ident initFn, $(attrs?.getD ∅),*] $(vis?)? $[unsafe%$unsafe?]?)
-      `(def initFn : IO $type := do $doSeq
-        $(⟨declModifiers⟩):declModifiers opaque $id : $type)
+      `($[unsafe%$unsafe?]? def initFn : IO $type := do $doSeq
+        $[$doc?:docComment]? @[$attrId:ident initFn, $(attrs?.getD ∅),*] $(vis?)? opaque $id : $type)
     else
-      if let `(Parser.Command.declModifiersT| ) := declModifiers then
-        `(@[$attrId:ident] def initFn : IO Unit := do $doSeq)
-      else
-        Macro.throwErrorAt declModifiers "invalid initialization command, unexpected modifiers"
+      let `(Parser.Command.declModifiersT| ) := declModifiers
+        | Macro.throwErrorAt declModifiers "invalid initialization command, unexpected modifiers"
+      `(@[$attrId:ident] def initFn : IO Unit := do $doSeq)
   | _ => Macro.throwUnsupported
 
 builtin_initialize
diff --git a/tests/lean/run/unsafeInit.lean b/tests/lean/run/unsafeInit.lean
new file mode 100644
index 0000000000..56e8afa975
--- /dev/null
+++ b/tests/lean/run/unsafeInit.lean
@@ -0,0 +1 @@
+unsafe initialize no : Nat ← pure lcUnreachable