diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index f5f9c79ad10b..2ae52461a0bf 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -953,7 +953,7 @@ Executes `x` tracking zetaDelta reductions `Config.trackZetaDelta := true`
   withConfig (fun cfg => { cfg with proofIrrelevance := false }) x
 
 @[inline] def withTransparency (mode : TransparencyMode) : n α → n α :=
-  mapMetaM <| withConfig (fun config => { config with transparency := mode })
+  withConfig (fun config => { config with transparency := mode })
 
 /-- `withDefault x` executes `x` using the default transparency setting. -/
 @[inline] def withDefault (x : n α) : n α :=
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index 78baf62bba53..1401e44c9027 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -879,10 +879,6 @@ def incDepth (mctx : MetavarContext) (allowLevelAssignments := false) : MetavarC
     if allowLevelAssignments then mctx.levelAssignDepth else depth
   { mctx with depth, levelAssignDepth }
 
-instance : MonadMCtx (StateRefT MetavarContext (ST ω)) where
-  getMCtx    := get
-  modifyMCtx := modify
-
 namespace MkBinding
 
 inductive Exception where
@@ -1275,10 +1271,10 @@ def mkBinding (isLambda : Bool) (xs : Array Expr) (e : Expr) (usedOnly : Bool :=
   MkBinding.mkBinding isLambda ctx.lctx xs e usedOnly usedLetOnly etaReduce { preserveOrder := false, binderInfoForMVars, mvarIdsToAbstract, mainModule := ctx.mainModule }
 
 @[inline] def mkLambda (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (etaReduce := false) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM Expr :=
-  return ← mkBinding (isLambda := true) xs e usedOnly usedLetOnly etaReduce binderInfoForMVars
+  mkBinding (isLambda := true) xs e usedOnly usedLetOnly etaReduce binderInfoForMVars
 
 @[inline] def mkForall (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM Expr :=
-  return ← mkBinding (isLambda := false) xs e usedOnly usedLetOnly false binderInfoForMVars
+  mkBinding (isLambda := false) xs e usedOnly usedLetOnly false binderInfoForMVars
 
 @[inline] def abstractRange (e : Expr) (n : Nat) (xs : Array Expr) : MkBindingM Expr := fun ctx =>
   MkBinding.abstractRange xs n e { preserveOrder := false, mainModule := ctx.mainModule }