diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index c986d185a1..df6c4f2432 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -255,7 +255,7 @@ where
      | some (α, lhs, rhs) =>
        let mut lhs := lhs
        let mut rhs := rhs
-       let mkMotive (typeWithLooseBVar : Expr) :=
+       let mkMotive (typeWithLooseBVar : Expr) := do
          withLocalDeclD (← mkFreshUserName `x) α fun x => do
            mkLambdaFVars #[x] $ typeWithLooseBVar.instantiate1 x
        let mut expectedAbst ← kabstract expectedType rhs