diff --git a/src/lake/Lake/Util/Opaque.lean b/src/lake/Lake/Util/Opaque.lean
index 943c60aeb3..062954fe99 100644
--- a/src/lake/Lake/Util/Opaque.lean
+++ b/src/lake/Lake/Util/Opaque.lean
@@ -9,8 +9,6 @@ prelude
 public import Init.Prelude
 import Init.Tactics
 
-namespace Lake
-
 opaque POpaque.nonemptyType.{u} : NonemptyType.{u}
 
 /-- An value of unknown type in a specific universe. -/
diff --git a/src/lake/Lake/Util/StoreInsts.lean b/src/lake/Lake/Util/StoreInsts.lean
index 9dd9f29e7a..971a05cc50 100644
--- a/src/lake/Lake/Util/StoreInsts.lean
+++ b/src/lake/Lake/Util/StoreInsts.lean
@@ -16,27 +16,27 @@ open Lean
 namespace Lake
 
 public instance {cmp : κ → κ → Ordering} [Monad m] [Std.LawfulEqCmp cmp] : MonadDStore κ β (StateT (Std.DTreeMap κ β cmp) m) where
-  fetch? k := return (← get).get? k
+  fetch? k := modifyGet fun m => (m.get? k, m)
   store k a := modify (·.insert k a)
 
 public instance {cmp : κ → κ → Ordering} [MonadLiftT (ST ω) m] [Monad m] [Std.LawfulEqCmp cmp] : MonadDStore κ β (StateRefT' ω (Std.DTreeMap κ β cmp) m) where
-  fetch? k := return (← get).get? k
+  fetch? k := modifyGet fun m => (m.get? k, m)
   store k a := modify (·.insert k a)
 
 public instance [Monad m] : MonadStore κ α (StateT (RBArray κ α cmp) m) where
-  fetch? k := return (← get).find? k
+  fetch? k := modifyGet fun m => (m.find? k, m)
   store k a := modify (·.insert k a)
 
 public instance [MonadLiftT (ST ω) m] [Monad m] : MonadStore κ α (StateRefT' ω (RBArray κ α cmp) m) where
-  fetch? k := return (← get).find? k
+  fetch? k := modifyGet fun m => (m.find? k, m)
   store k a := modify (·.insert k a)
 
 public instance [Monad m] : MonadStore Name α (StateT (NameMap α) m) where
-  fetch? k := return (← get).find? k
+  fetch? k := modifyGet fun m => (m.find? k, m)
   store k a := modify (·.insert k a)
 
 public instance [MonadLiftT (ST ω) m] [Monad m] : MonadStore Name α (StateRefT' ω (NameMap α) m) where
-  fetch? k := return (← get).find? k
+  fetch? k := modifyGet fun m => (m.find? k, m)
   store k a := modify (·.insert k a)
 
 public instance [MonadDStore κ β m] [t : FamilyOut β k α] : MonadStore1Of k α m where