From 2b453de299c26217914feec70d1063ace3dd7c85 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 18 Jun 2019 15:25:34 -0700
Subject: [PATCH] fix(frontends/lean/decl_attributes): remove mdata

---
 src/frontends/lean/decl_attributes.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp
index d5a3495bed..9d8f8afc62 100644
--- a/src/frontends/lean/decl_attributes.cpp
+++ b/src/frontends/lean/decl_attributes.cpp
@@ -80,7 +80,10 @@ syntax decl_attributes::expr_to_syntax(expr const & e) {
     buffer<expr> args;
     get_app_args(e, args);
     buffer<syntax> new_args;
-    for (expr const & arg : args) {
+    for (expr arg : args) {
+        while (is_mdata(arg)) {
+            arg = mdata_expr(arg);
+        }
         if (is_constant(arg)) {
             new_args.push_back(mk_syntax_ident(const_name(arg)));
         } else if (is_lit(arg)) {