diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index b19fa5f452..aca4585bc6 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -636,7 +636,7 @@ else
   let optUnivDeclStx := declId.getArg 1;
   (id, optUnivDeclStx)
 
-@[inline] def withDeclId (declId : Syntax) (f : Name → CommandElabM Unit) : CommandElabM Unit := do
+def withDeclId {α} (declId : Syntax) (f : Name → CommandElabM α) : CommandElabM α := do
 -- ident >> optional (".{" >> sepBy1 ident ", " >> "}")
 let (id, optUnivDeclStx) := expandDeclId declId;
 savedLevelNames ← getLevelNames;