From 8f824ce14133230a7ec7cbcec6bc4babd68cb06b Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 13 Mar 2021 13:17:13 +0100
Subject: [PATCH] fix: KeyedDeclsAttribute: preserve scopedness

---
 src/Lean/KeyedDeclsAttribute.lean | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean
index 9e31ba9263..6b8921d025 100644
--- a/src/Lean/KeyedDeclsAttribute.lean
+++ b/src/Lean/KeyedDeclsAttribute.lean
@@ -125,13 +125,12 @@ protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name) : IO (KeyedDe
       applicationTime := AttributeApplicationTime.afterCompilation
     }
   registerBuiltinAttribute {
-    name            := df.name,
-    descr           := df.descr,
-    add             := fun constName stx persistent => do
+    name            := df.name
+    descr           := df.descr
+    add             := fun constName stx attrKind => do
       let key ← df.evalKey false stx
       let val ← evalConstCheck γ df.valueTypeName constName
-      let env ← getEnv
-      setEnv <| ext.addEntry env { key := key, decl := constName, value := val },
+      ext.add { key := key, decl := constName, value := val } attrKind
     applicationTime := AttributeApplicationTime.afterCompilation
   }
   pure { defn := df, tableRef := tableRef, ext := ext }