From fc26c8145c730d24eb3946c7019d7cf83a9e3b51 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 12 Dec 2025 09:56:08 +0100
Subject: [PATCH] chore: realization of private def should run in private scope
 (#11618)

In fact the scope should be solely determined by the def name but this
breaks some existing realizer, so postponed.
---
 src/Lean/Meta/Basic.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index f2cddd270a..84901ef65b 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -2673,7 +2673,8 @@ where
         let _ : MonadExceptOf _ MetaM := MonadAlwaysExcept.except
         observing do
           withDeclNameForAuxNaming constName do
-            realize
+            withoutExporting (when := isPrivateName constName) do
+              realize
           -- Meta code working on a non-exported declaration should usually do so inside
           -- `withoutExporting` but we're lenient here in case this call is the only one that needs
           -- the setting.