diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean
index 14de0c820c..162cefa991 100644
--- a/src/Lean/PrettyPrinter.lean
+++ b/src/Lean/PrettyPrinter.lean
@@ -25,17 +25,14 @@ def ppTerm (stx : Syntax) : CoreM Format := do
   let stx := (sanitizeSyntax stx).run' { options := opts }
   parenthesizeTerm stx >>= formatTerm
 
-def ppExpr (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) : MetaM Format := do
-  let lctx ← getLCtx
-  let opts ← getOptions
-  let lctx := lctx.sanitizeNames.run' { options := opts }
+def ppExpr (e : Expr) : MetaM Format := do
+  let lctx := (← getLCtx).sanitizeNames.run' { options := (← getOptions) }
   Meta.withLCtx lctx #[] do
-    let stx ← delab currNamespace openDecls e
-    ppTerm stx
+    ppTerm (← delab e)
 
 @[export lean_pp_expr]
 def ppExprLegacy (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : IO Format :=
-  Prod.fst <$> ((ppExpr Name.anonymous [] e).run' { lctx := lctx } { mctx := mctx }).toIO { options := opts } { env := env }
+  Prod.fst <$> ((ppExpr e).run' { lctx := lctx } { mctx := mctx }).toIO { options := opts } { env := env }
 
 def ppCommand (stx : Syntax) : CoreM Format :=
   parenthesizeCommand stx >>= formatCommand
@@ -61,7 +58,7 @@ private def withoutContext {m} [MonadExcept Exception m] (x : m Format) : m Form
 
 builtin_initialize
   ppFnsRef.set {
-    ppExpr := fun ctx e      => ctx.runMetaM <| withoutContext <| ppExpr ctx.currNamespace ctx.openDecls e,
+    ppExpr := fun ctx e      => ctx.runMetaM <| withoutContext <| ppExpr e,
     ppTerm := fun ctx stx    => ctx.runCoreM <| withoutContext <| ppTerm stx,
     ppGoal := fun ctx mvarId => ctx.runMetaM <| withoutContext <| Meta.ppGoal mvarId
   }
diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index d4e62fce38..fa35c149ed 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -263,7 +263,7 @@ end Delaborator
 
 open Delaborator (OptionsPerPos topDownAnalyze Pos)
 
-def delabCore (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (optionsPerPos : OptionsPerPos := {}) : MetaM (Syntax × Std.RBMap Pos Elab.Info compare) := do
+def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) : MetaM (Syntax × Std.RBMap Pos Elab.Info compare) := do
   trace[PrettyPrinter.delab.input] "{Std.format e}"
   let mut opts ← MonadOptions.getOptions
   -- default `pp.proofs` to `true` if `e` is a proof
@@ -279,8 +279,8 @@ def delabCore (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (opt
     (Delaborator.delab
       { defaultOptions := opts
         optionsPerPos := optionsPerPos
-        currNamespace := currNamespace
-        openDecls := openDecls
+        currNamespace := (← getCurrNamespace)
+        openDecls := (← getOpenDecls)
         subExpr := Delaborator.SubExpr.mkRoot e
         inPattern := opts.getInPattern }
       |>.run { : Delaborator.State })
@@ -288,8 +288,8 @@ def delabCore (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (opt
   return (stx, infos)
 
 /-- "Delaborate" the given term into surface-level syntax using the default and given subterm-specific options. -/
-def delab (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (optionsPerPos : OptionsPerPos := {}) : MetaM Syntax := do
-  let (stx, _) ← delabCore currNamespace openDecls e optionsPerPos
+def delab (e : Expr) (optionsPerPos : OptionsPerPos := {}) : MetaM Syntax := do
+  let (stx, _) ← delabCore e optionsPerPos
   return stx
 
 builtin_initialize registerTraceClass `PrettyPrinter.delab
diff --git a/src/Lean/Server/Rpc/Deriving.lean b/src/Lean/Server/Rpc/Deriving.lean
index 20ee017686..060212b056 100644
--- a/src/Lean/Server/Rpc/Deriving.lean
+++ b/src/Lean/Server/Rpc/Deriving.lean
@@ -81,7 +81,7 @@ private def deriveInstance (typeName : Name) : CommandElabM Bool := do
         let fieldT ← inferType x
         let some fieldEncT ← hasRpcEncoding? fieldT
           | throwError "cannot synthesize 'RpcEncoding {fieldT} ?_'"
-        let fieldEncTStx ← PrettyPrinter.delab (← getCurrNamespace) (← getOpenDecls) fieldEncT
+        let fieldEncTStx ← PrettyPrinter.delab fieldEncT
         fieldEncTs := fieldEncTs.push fieldEncTStx
 
       let typeId := mkIdent typeName
diff --git a/src/Lean/Widget/InteractiveCode.lean b/src/Lean/Widget/InteractiveCode.lean
index 6fc29526ad..22e4cc93fe 100644
--- a/src/Lean/Widget/InteractiveCode.lean
+++ b/src/Lean/Widget/InteractiveCode.lean
@@ -75,11 +75,9 @@ where
 open PrettyPrinter in
 private def formatWithOpts (e : Expr) (optsPerPos : Delaborator.OptionsPerPos)
     : MetaM (Format × Std.RBMap Nat Elab.Info compare) := do
-    let currNamespace ← getCurrNamespace
-    let openDecls ← getOpenDecls
     let opts ← getOptions
     let e ← Meta.instantiateMVars e
-    let (stx, infos) ← PrettyPrinter.delabCore currNamespace openDecls e optsPerPos
+    let (stx, infos) ← PrettyPrinter.delabCore e optsPerPos
     let stx := sanitizeSyntax stx |>.run' { options := opts }
     let stx ← PrettyPrinter.parenthesizeTerm stx
     let fmt ← PrettyPrinter.formatTerm stx
diff --git a/tests/lean/625.lean b/tests/lean/625.lean
index 82546e0d5e..e11a8d684b 100644
--- a/tests/lean/625.lean
+++ b/tests/lean/625.lean
@@ -8,11 +8,11 @@ def px   : PUnit := ()
 
 #eval show MetaM Format from do
   let e : Expr := mkApp (mkMData {} $ mkConst `foo [levelOne]) (mkConst `x)
-  formatTerm (← delab Name.anonymous [] e)
+  formatTerm (← delab e)
 
 #eval show MetaM Format from do
   let opts := ({}: Options).setBool `pp.universes true
   -- the MData annotation should make it not a regular application,
   -- so the unexpander should not be called.
   let e : Expr := mkApp (mkMData opts $ mkConst `foo [levelOne]) (mkConst `x)
-  formatTerm (← delab Name.anonymous [] e)
+  formatTerm (← delab e)
diff --git a/tests/lean/PPRoundtrip.lean b/tests/lean/PPRoundtrip.lean
index ed1646454d..0ee518c053 100644
--- a/tests/lean/PPRoundtrip.lean
+++ b/tests/lean/PPRoundtrip.lean
@@ -14,7 +14,7 @@ def checkM (stx : TermElabM Syntax) (optionsPerPos : OptionsPerPos := {}) : Term
 let opts ← getOptions
 let stx ← stx
 let e ← elabTermAndSynthesize stx none <* throwErrorIfErrors
-let stx' ← delab Name.anonymous [] e optionsPerPos
+let stx' ← delab e optionsPerPos
 let f' ← PrettyPrinter.ppTerm stx'
 let s := f'.pretty' opts
 IO.println s
diff --git a/tests/lean/ppExpr.lean b/tests/lean/ppExpr.lean
index dcb3a8c19c..6385fb6d65 100644
--- a/tests/lean/ppExpr.lean
+++ b/tests/lean/ppExpr.lean
@@ -6,7 +6,7 @@ import Lean
 open Lean
 
 def test (e : Expr) : MetaM Unit := do
-  IO.println (← PrettyPrinter.ppExpr Name.anonymous [] e)
+  IO.println (← PrettyPrinter.ppExpr e)
 
 -- loose bound variable
 #eval test (mkBVar 0)
diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean
index 54c51f5c8e..171ab448d1 100644
--- a/tests/lean/run/PPTopDownAnalyze.lean
+++ b/tests/lean/run/PPTopDownAnalyze.lean
@@ -12,7 +12,7 @@ open Lean.PrettyPrinter
 def checkDelab (e : Expr) (tgt? : Option Syntax) (name? : Option Name := none) : TermElabM Unit := do
   let pfix := "[checkDelab" ++ (match name? with | some n => ("." ++ toString n) | none => "") ++ "]"
   if e.hasMVar then throwError "{pfix} original term has mvars, {e}"
-  let stx ← delab (← getCurrNamespace) (← getOpenDecls) e
+  let stx ← delab e
   match tgt? with
   | some tgt =>
     if toString (← PrettyPrinter.ppTerm stx) != toString (← PrettyPrinter.ppTerm tgt?.get!) then