diff --git a/Qq/Macro.lean b/Qq/Macro.lean
index f2e52b3..9389156 100644
--- a/Qq/Macro.lean
+++ b/Qq/Macro.lean
@@ -495,7 +495,7 @@ def Impl.macro (t : Syntax) (expectedType : Expr) : TermElabM Expr := do
       withProcessPostponed do withSynthesize do
       let t ← Term.elabTerm t lastDecl.type
       let t ← ensureHasType lastDecl.type t
-      synthesizeSyntheticMVars (mayPostpone := false)
+      synthesizeSyntheticMVars (postpone := .no)
       if (← logUnassignedUsingErrorInfos (← getMVars t)) then
         throwAbortTerm
       lastId.assign t
diff --git a/Qq/Match.lean b/Qq/Match.lean
index abe4cfc..442faf9 100644
--- a/Qq/Match.lean
+++ b/Qq/Match.lean
@@ -172,7 +172,7 @@ def elabPat (pat : Term) (lctx : LocalContext) (localInsts : LocalInstances) (ty
           let (pat, patVars) ← getPatVars pat #[]
           let pat ← Lean.Elab.Term.elabTerm pat ty
           let pat ← ensureHasType ty pat
-          synthesizeSyntheticMVars false
+          synthesizeSyntheticMVars (postpone := .no)
           let pat ← instantiateMVars pat
 
           let mctx ← getMCtx
diff --git a/lean-toolchain b/lean-toolchain
index cfcdd32..0ba3faf 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.6.0-rc1
+leanprover/lean4:v4.9.0-rc1