diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index 5165eb64c5..70fecd0ee6 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -177,7 +177,7 @@ inductive AliasValue (α : Type) where
 abbrev AliasTable (α) := NameMap (AliasValue α)
 
 def registerAliasCore {α} (mapRef : IO.Ref (AliasTable α)) (aliasName : Name) (value : AliasValue α) : IO Unit := do
-  unless (← IO.initializing) do throw ↑"aliases can only be registered during initialization"
+  unless (← initializing) do throw ↑"aliases can only be registered during initialization"
   if (← mapRef.get).contains aliasName then
     throw ↑s!"alias '{aliasName}' has already been declared"
   mapRef.modify (·.insert aliasName value)
diff --git a/src/Lean/Server/Rpc/RequestHandling.lean b/src/Lean/Server/Rpc/RequestHandling.lean
index 75614e7e3c..2c7293329f 100644
--- a/src/Lean/Server/Rpc/RequestHandling.lean
+++ b/src/Lean/Server/Rpc/RequestHandling.lean
@@ -93,7 +93,7 @@ def registerBuiltinRpcProcedure (method : Name) paramType respType
     [RpcEncodable paramType] [RpcEncodable respType]
     (handler : paramType → RequestM (RequestTask respType)) : IO Unit := do
   let errMsg := s!"Failed to register builtin RPC call handler for '{method}'"
-  unless (← IO.initializing) do
+  unless (← initializing) do
     throw <| IO.userError s!"{errMsg}: only possible during initialization"
   if (←builtinRpcProcedures.get).contains method then
     throw <| IO.userError s!"{errMsg}: already registered"