diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean
index 26ce7f9c1e..34b4e25726 100644
--- a/src/Lean/Parser/Syntax.lean
+++ b/src/Lean/Parser/Syntax.lean
@@ -70,8 +70,8 @@ def macroArgType   := nonReservedSymbol "ident" <|> nonReservedSymbol "num" <|>
 def macroArgSimple := parser! ident >> checkNoWsBefore "no space before ':'" >> ":" >> macroArgType
 def macroArg  := try strLit <|> try macroArgSimple
 def macroHead := macroArg <|> try ident
-def macroTailTactic   : Parser := try (" : " >> identEq "tactic") >> darrow >> "`(" >> sepBy1 tacticParser "; " true true >> ")"
-def macroTailCommand  : Parser := try (" : " >> identEq "command") >> darrow >> "`(" >> many1 commandParser true >> ")"
+def macroTailTactic   : Parser := try (" : " >> identEq "tactic") >> darrow >> ("`(" >> sepBy1 tacticParser "; " true true >> ")" <|> termParser)
+def macroTailCommand  : Parser := try (" : " >> identEq "command") >> darrow >> ("`(" >> many1 commandParser true >> ")" <|> termParser)
 def macroTailDefault  : Parser := try (" : " >> ident) >> darrow >> (("`(" >> categoryParserOfStack 2 >> ")") <|> termParser)
 def macroTail := macroTailTactic <|> macroTailCommand <|> macroTailDefault
 @[builtinCommandParser] def «macro»       := parser! "macro " >> optPrecedence >> macroHead >> many macroArg >> macroTail