diff --git a/src/Lean/Meta/AbstractNestedProofs.lean b/src/Lean/Meta/AbstractNestedProofs.lean
index 9ad124f04d8e..b63d05e2c8bf 100644
--- a/src/Lean/Meta/AbstractNestedProofs.lean
+++ b/src/Lean/Meta/AbstractNestedProofs.lean
@@ -107,6 +107,8 @@ def abstractNestedProofs (e : Expr) (cache := true) : MetaM Expr := do
     -- `e` is a proof itself. So, we don't abstract nested proofs
     return e
   else
-    AbstractNestedProofs.visit e |>.run { cache } |>.run
+    withTransparency TransparencyMode.all <|
+    withInferTypeConfig <|
+        AbstractNestedProofs.visit e |>.run { cache } |>.run
 
 end Lean.Meta