From be02133ca79f667abdc2764ce827faaa4b1867cc Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@protonmail.com>
Date: Sat, 31 Jul 2021 18:45:33 -0700
Subject: [PATCH] feat: pp.analyze default transparency

---
 src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index bea960066d..7f48c0635c 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -192,8 +192,7 @@ def isDefEqAssigning (t s : Expr) : MetaM Bool := do
 
 def checkpointDefEq (t s : Expr) : MetaM Bool := do
   Meta.checkpointDefEq (mayPostpone := false) do
-    withTransparency TransparencyMode.instances do
-      isDefEqAssigning t s
+    isDefEqAssigning t s
 
 def tryUnify (t s : Expr) : MetaM Unit := do
   try