diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 6a40963d01..d02b03d5db 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -270,15 +270,6 @@ let lvlCtx : Level.Context := { fileName := ctx.fileName, fileMap := ctx.fileMap
 def elabLevel (stx : Syntax) : TermElabM Level :=
 liftLevelM $ Level.elabLevel stx
 
-@[inline] def withConfig {α} (f : Meta.Config → Meta.Config) (x : TermElabM α) : TermElabM α :=
-adaptTheReader Meta.Context (fun (ctx : Meta.Context) => { ctx with config := f ctx.config }) x
-
-@[inline] def withTransparency {α} (mode : Meta.TransparencyMode) (x : TermElabM α) : TermElabM α :=
-withConfig (fun config => { config with transparency := mode }) x
-
-@[inline] def withReducible {α} (x : TermElabM α) : TermElabM α :=
-withTransparency Meta.TransparencyMode.reducible x
-
 /- Elaborate `x` with `stx` on the macro stack -/
 @[inline] def withMacroExpansion {α} (beforeStx afterStx : Syntax) (x : TermElabM α) : TermElabM α :=
 adaptReader (fun (ctx : Context) => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x