diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean
index cdd3be8ded..1c5dc2ce93 100644
--- a/src/Lean/ResolveName.lean
+++ b/src/Lean/ResolveName.lean
@@ -105,13 +105,13 @@ let rec loop : Name → List String → List (Name × List String)
       | some newId => [(newId, projs)]
       | none =>
         let resolvedIds := if env.contains id then [id] else []
-        let idPrv := mkPrivateName env id
+        let idPrv       := mkPrivateName env id
         let resolvedIds := if env.contains idPrv then [idPrv] ++ resolvedIds else resolvedIds
         let resolvedIds := resolveOpenDecls env id openDecls resolvedIds
         let resolvedIds := getAliases env id ++ resolvedIds
         match resolvedIds with
-        | resolvedIds@(_ :: _) => resolvedIds.eraseDups.map fun id => (id, projs)
-        | []                   => loop p (s::projs)
+        | _ :: _ => resolvedIds.eraseDups.map fun id => (id, projs)
+        | []     => loop p (s::projs)
   | _, _ => []
 loop extractionResult.name []
 
@@ -189,7 +189,7 @@ variables [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m]
 def resolveNamespace (id : Name) : m Name := do
 match ResolveName.resolveNamespace? (← getEnv) (← getCurrNamespace) (← getOpenDecls) id with
 | some ns => return ns
-| none    => throwError ("unknown namespace '" ++ id ++ "'")
+| none    => throwError s!"unknown namespace '{id}'"
 
 /- Similar to `resolveGlobalName`, but discard any candidate whose `fieldList` is not empty. -/
 def resolveGlobalConst (n : Name) : m (List Name) := do