diff --git a/src/Lean/Elab/Tactic/Config.lean b/src/Lean/Elab/Tactic/Config.lean
index af97c69b78..3c949b5f3e 100644
--- a/src/Lean/Elab/Tactic/Config.lean
+++ b/src/Lean/Elab/Tactic/Config.lean
@@ -16,9 +16,11 @@ macro "declare_config_elab" elabName:ident type:ident : command =>
      if optConfig.isNone then
        return { : $type }
      else
-       withoutModifyingState <| withLCtx {} {} <| withSaveInfoContext <| Term.withSynthesize do
+       let c ← withoutModifyingState <| withLCtx {} {} <| withSaveInfoContext <| Term.withSynthesize do
          let c ← Term.elabTermEnsuringType optConfig[0][3] (Lean.mkConst ``$type)
-         eval (← instantiateMVars c)
+         Term.synthesizeSyntheticMVarsNoPostponing
+         instantiateMVars c
+       eval c
   )
 
 end Lean.Elab.Tactic
diff --git a/tests/lean/run/declareConfigElabIssue.lean b/tests/lean/run/declareConfigElabIssue.lean
new file mode 100644
index 0000000000..bdc2fc5509
--- /dev/null
+++ b/tests/lean/run/declareConfigElabIssue.lean
@@ -0,0 +1,2 @@
+example : True := by
+  simp (config := (fun (c : Lean.Meta.Simp.Config) => { c with arith := true }) {})