diff --git a/src/Lean/Elab/Tactic/Unfold.lean b/src/Lean/Elab/Tactic/Unfold.lean
index 1ce9a864dc..64d9451459 100644
--- a/src/Lean/Elab/Tactic/Unfold.lean
+++ b/src/Lean/Elab/Tactic/Unfold.lean
@@ -20,8 +20,15 @@ def unfoldTarget (declName : Name) : TacticM Unit := do
   "unfold " ident (location)?
 -/
 @[builtinTactic Lean.Parser.Tactic.unfold] def evalUnfold : Tactic := fun stx => do
-  let declName ← resolveGlobalConstNoOverload stx[1]
   let loc := expandOptLocation stx[2]
-  withLocation loc (unfoldLocalDecl declName) (unfoldTarget declName) (throwTacticEx `unfold · m!"did not unfold '{declName}'")
+  if stx[1].isIdent then
+    go stx[1] loc
+  else
+    for declNameId in stx[1].getSepArgs do
+      go declNameId loc
+where
+  go (declNameId : Syntax) (loc : Location) : TacticM Unit := do
+    let declName ← resolveGlobalConstNoOverload declNameId
+    withLocation loc (unfoldLocalDecl declName) (unfoldTarget declName) (throwTacticEx `unfold · m!"did not unfold '{declName}'")
 
 end Lean.Elab.Tactic