diff --git a/src/frontends/lean/vm_elaborator.cpp b/src/frontends/lean/vm_elaborator.cpp
index a7fe38310a..fde1837e9a 100644
--- a/src/frontends/lean/vm_elaborator.cpp
+++ b/src/frontends/lean/vm_elaborator.cpp
@@ -164,17 +164,7 @@ decl_attributes to_decl_attributes(environment const & env, expr const & e, bool
         buffer<expr> args;
         auto attr = get_app_args(e, args);
         auto n = const_name(attr);
-        if (n == "recursor") {
-            list<unsigned> idxs;
-            for (int i = args.size() - 1; i >= 0; i--)
-                idxs = cons(lit_value(unwrap_pos(args[i])).get_nat().get_small_value() - 1, idxs);
-            attributes.set_attribute(env, n, attr_data_ptr(new indices_attribute_data(idxs)));
-        } else if (n == "extern") {
-            // TODO(Sebastian): implement in C++ or Lean
-        } else {
-            lean_assert(args.empty());
-            attributes.set_attribute(env, n);
-        }
+        attributes.set_attribute(env, n, get_attribute(env, n).parse_data(e));
     }
     return attributes;
 }