From 4b84f8fa882c8e7d3beef3a2ee5dc0d8bb3e05a6 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 16 Jun 2020 21:59:40 +0200
Subject: [PATCH] fix: nullary attributes in new frontend

---
 src/Lean/Elab/DeclModifiers.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean
index aedbd65539..7ff13d7053 100644
--- a/src/Lean/Elab/DeclModifiers.lean
+++ b/src/Lean/Elab/DeclModifiers.lean
@@ -64,6 +64,8 @@ env ← getEnv;
 unless (isAttribute env attrName) $
   throwError stx ("unknown attribute [" ++ attrName ++ "]");
 let args := stx.getArg 1;
+-- the old frontend passes Syntax.missing for empty args, for reasons
+let args := if args.getNumArgs == 0 then Syntax.missing else args;
 pure { name := attrName, args := args }
 
 def elabAttrs (stx : Syntax) : CommandElabM (Array Attribute) :=