diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean
index ecd593baa3..238f3074a1 100644
--- a/src/Lean/Meta/Eqns.lean
+++ b/src/Lean/Meta/Eqns.lean
@@ -80,7 +80,7 @@ private def mkSimpleEqThm (declName : Name) : MetaM (Option Name) := do
   By default, we not create equation theorems for nonrecursive definitions.
   You can use `nonRec := true` to override this behavior, a dummy `rfl` proof is created on the fly.
 -/
-def getEqnsFor? (declName : Name) (nonRec := false) : MetaM (Option (Array Name)) := do
+def getEqnsFor? (declName : Name) (nonRec := false) : MetaM (Option (Array Name)) := withLCtx {} {} do
   if let some eqs := eqnsExt.getState (← getEnv) |>.map.find? declName then
     return some eqs
   else if (← shouldGenerateEqnThms declName) then
@@ -134,7 +134,7 @@ def registerGetUnfoldEqnFn (f : GetUnfoldEqnFn) : IO Unit := do
   By default, we not create unfold theorems for nonrecursive definitions.
   You can use `nonRec := true` to override this behavior.
 -/
-def getUnfoldEqnFor? (declName : Name) (nonRec := false) : MetaM (Option Name) := do
+def getUnfoldEqnFor? (declName : Name) (nonRec := false) : MetaM (Option Name) := withLCtx {} {} do
   if (← shouldGenerateEqnThms declName) then
     for f in (← getUnfoldEqnFnsRef.get) do
       if let some r ← f declName then
diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean
index 4a44d4c505..1f57f9ad09 100644
--- a/src/Lean/Meta/Match/MatchEqs.lean
+++ b/src/Lean/Meta/Match/MatchEqs.lean
@@ -260,7 +260,7 @@ private def substSomeVar (mvarId : MVarId) : MetaM (Array MVarId) := withMVarCon
   the `match`-eliminator `matchDeclName`. `type` contains the type of the theorem. -/
 partial def proveCondEqThm (matchDeclName : Name) (type : Expr) : MetaM Expr := do
   let type ← instantiateMVars type
-  withLCtx {} {} <| forallTelescope type fun ys target => do
+  forallTelescope type fun ys target => do
     let mvar0  ← mkFreshExprSyntheticOpaqueMVar target
     let mvarId ← deltaTarget mvar0.mvarId! (· == matchDeclName)
     trace[Meta.Match.matchEqs] "{MessageData.ofGoal mvarId}"
@@ -397,7 +397,7 @@ where
 
 /--
   Create conditional equations and splitter for the given match auxiliary declaration. -/
-private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns := do
+private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns := withLCtx {} {} do
   trace[Meta.Match.matchEqs] "mkEquationsFor '{matchDeclName}'"
   withConfig (fun c => { c with etaStruct := .none }) do
   let baseName := mkPrivateName (← getEnv) matchDeclName
diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
index a09735275c..54b1a19efc 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
@@ -383,17 +383,16 @@ where
       else
         return none
 
-def SimpTheorems.addDeclToUnfold (d : SimpTheorems) (declName : Name) : MetaM SimpTheorems :=
-  withLCtx {} {} do
-    if let some eqns ← getEqnsFor? declName then
-      let mut d := d
-      for eqn in eqns do
-        d ← SimpTheorems.addConst d eqn
-      if hasSmartUnfoldingDecl (← getEnv) declName then
-        d := d.addDeclToUnfoldCore declName
-      return d
-    else
-      return d.addDeclToUnfoldCore declName
+def SimpTheorems.addDeclToUnfold (d : SimpTheorems) (declName : Name) : MetaM SimpTheorems := do
+  if let some eqns ← getEqnsFor? declName then
+    let mut d := d
+    for eqn in eqns do
+      d ← SimpTheorems.addConst d eqn
+    if hasSmartUnfoldingDecl (← getEnv) declName then
+      d := d.addDeclToUnfoldCore declName
+    return d
+  else
+    return d.addDeclToUnfoldCore declName
 
 abbrev SimpTheoremsArray := Array SimpTheorems