diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean
index 5dda5df5a0..fb6186a5d4 100644
--- a/src/Init/Lean/Meta/Basic.lean
+++ b/src/Init/Lean/Meta/Basic.lean
@@ -726,6 +726,11 @@ do mvarDecl ← getMVarDecl mvarId;
      else
        resettingSynthInstanceCache x
 
+@[inline] def withMCtx {α} (mctx : MetavarContext) (x : MetaM α) : MetaM α :=
+do mctx' ← getMCtx;
+   modify $ fun s => { mctx := mctx, .. s };
+   finally x (modify $ fun s => { mctx := mctx', .. s })
+
 end Meta
 end Lean