diff --git a/src/Init/Lean/Elab/Syntax.lean b/src/Init/Lean/Elab/Syntax.lean
index 1feddd5428..e955383881 100644
--- a/src/Init/Lean/Elab/Syntax.lean
+++ b/src/Init/Lean/Elab/Syntax.lean
@@ -247,18 +247,6 @@ adaptExpander $ fun stx => match_syntax stx with
   `(syntax [$(mkIdentFrom stx kind)] $syntaxParts* : $cat macro_rules | `($pat) => `($rhs))
 | _ => throwUnsupportedSyntax
 
-/- Convert `macro` head into a `syntax` command item -/
-def expandMacroHeadIntoSyntaxItem (stx : Syntax) : CommandElabM Syntax :=
-let k := stx.getKind;
-if k == `Lean.Parser.Command.identPrec then
-  let info := stx.getHeadInfo;
-  let id   := (stx.getArg 0).getId;
-  pure $ Syntax.node `Lean.Parser.Syntax.atom #[mkStxStrLit (toString id) info, stx.getArg 1]
-else if k == `Lean.Parser.Command.strLitPrec then
-  pure $ Syntax.node `Lean.Parser.Syntax.atom stx.getArgs
-else
-  throwUnsupportedSyntax
-
 /- Convert `macro` argument into a `syntax` command item -/
 def expandMacroArgIntoSyntaxItem (stx : Syntax) : CommandElabM Syntax :=
 let k := stx.getKind;
@@ -276,16 +264,15 @@ else if k == `Lean.Parser.Command.strLitPrec then
 else
   throwUnsupportedSyntax
 
-/- Convert `macro` head into a pattern element -/
-def expandMacroHeadIntoPattern (stx : Syntax) : CommandElabM Syntax :=
+/- Convert `macro` head into a `syntax` command item -/
+def expandMacroHeadIntoSyntaxItem (stx : Syntax) : CommandElabM Syntax :=
 let k := stx.getKind;
 if k == `Lean.Parser.Command.identPrec then
-  let str := toString (stx.getArg 0).getId;
-  pure $ mkAtomFrom stx str
-else if k == `Lean.Parser.Command.strLitPrec then
-  strLitPrecToPattern stx
+  let info := stx.getHeadInfo;
+  let id   := (stx.getArg 0).getId;
+  pure $ Syntax.node `Lean.Parser.Syntax.atom #[mkStxStrLit (toString id) info, stx.getArg 1]
 else
-  throwUnsupportedSyntax
+  expandMacroArgIntoSyntaxItem stx
 
 /- Convert `macro` arg into a pattern element -/
 def expandMacroArgIntoPattern (stx : Syntax) : CommandElabM Syntax :=
@@ -298,6 +285,15 @@ else if k == `Lean.Parser.Command.strLitPrec then
 else
   throwUnsupportedSyntax
 
+/- Convert `macro` head into a pattern element -/
+def expandMacroHeadIntoPattern (stx : Syntax) : CommandElabM Syntax :=
+let k := stx.getKind;
+if k == `Lean.Parser.Command.identPrec then
+  let str := toString (stx.getArg 0).getId;
+  pure $ mkAtomFrom stx str
+else
+  expandMacroArgIntoPattern stx
+
 @[builtinCommandElab «macro»] def elabMacro : CommandElab :=
 adaptExpander $ fun stx => do
   let head    := stx.getArg 1;
diff --git a/src/Init/Lean/Parser/Syntax.lean b/src/Init/Lean/Parser/Syntax.lean
index 88f628537b..f9f46ae6e4 100644
--- a/src/Init/Lean/Parser/Syntax.lean
+++ b/src/Init/Lean/Parser/Syntax.lean
@@ -65,9 +65,9 @@ def identPrec  := parser! ident >> optPrecedence
 @[builtinCommandParser] def «syntax»      := parser! "syntax " >> optional ("[" >> ident >> "]") >> many1 syntaxParser >> " : " >> ident
 @[builtinCommandParser] def syntaxCat     := parser! "declare_syntax_cat " >> ident
 def macroArgType   := nonReservedSymbol "ident" <|> nonReservedSymbol "num" <|> nonReservedSymbol "str" <|> nonReservedSymbol "char" <|> (ident >> optPrecedence)
-def macroArgSimple := parser! ident >> ":" >> macroArgType
+def macroArgSimple := parser! ident >> checkNoWsBefore "no space before ':'" >> ":" >> macroArgType
 def macroArg  := try strLitPrec <|> try macroArgSimple
-def macroHead := try strLitPrec <|> try identPrec
+def macroHead := macroArg <|> try identPrec
 def macroTailTactic   : Parser := try (" : " >> identEq "tactic") >> darrow >> "`(" >> sepBy1 tacticParser "; " true true >> ")"
 def macroTailCommand  : Parser := try (" : " >> identEq "command") >> darrow >> "`(" >> many1 commandParser true >> ")"
 def macroTailDefault  : Parser := try (" : " >> ident) >> darrow >> "`(" >> categoryParserOfStack 2 >> ")"
diff --git a/tests/lean/run/kevin.lean b/tests/lean/run/kevin.lean
new file mode 100644
index 0000000000..a3c647439c
--- /dev/null
+++ b/tests/lean/run/kevin.lean
@@ -0,0 +1,6 @@
+import Init.Lean
+new_frontend
+open Lean
+
+macro x:term "ⁿ":10000 : term => `($x ^ $(mkTermId (mkNameSimple "n")))
+#check fun (n : Nat) => nⁿ