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