diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 57a6c9e5b..2ee9d3334 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -71,12 +71,7 @@ static void print_axioms(parser & p) {
     environment const & env = p.env();
     env.for_each_declaration([&](declaration const & d) {
             name const & n = d.get_name();
-            if (!d.is_definition() &&
-                !is_quotient_decl(env, n) &&
-                !is_hits_decl(env, n) &&
-                !inductive::is_inductive_decl(env, n) &&
-                !inductive::is_elim_rule(env, n) &&
-                !inductive::is_intro_rule(env, n)) {
+            if (!d.is_definition() && !env.is_builtin(n)) {
                 p.regular_stream() << n << " : " << d.get_type() << endl;
                 has_axioms = true;
             }
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index bd3e586fe..f98ef6c9d 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -57,6 +57,7 @@ public:
     bool impredicative() const { return m_impredicative; }
     normalizer_extension const & norm_ext() const { return *(m_norm_ext.get()); }
     bool is_recursor(environment const & env, name const & n) const { return m_norm_ext->is_recursor(env, n); }
+    bool is_builtin(environment const & env, name const & n) const { return m_norm_ext->is_builtin(env, n); }
 };
 
 class environment_extension {
@@ -137,6 +138,8 @@ public:
 
     bool is_recursor(name const & n) const { return m_header->is_recursor(*this, n); }
 
+    bool is_builtin(name const & n) const { return m_header->is_builtin(*this, n); }
+
     /** \brief Return true iff the environment treats universe level 0 as an impredicative Prop */
     bool impredicative() const { return m_header->impredicative(); }
 
diff --git a/src/kernel/hits/hits.cpp b/src/kernel/hits/hits.cpp
index ed50b742f..8c70dca73 100644
--- a/src/kernel/hits/hits.cpp
+++ b/src/kernel/hits/hits.cpp
@@ -133,6 +133,10 @@ bool hits_normalizer_extension::is_recursor(environment const &, name const & n)
     return n == *g_trunc_rec || n == *g_type_quotient_rec;
 }
 
+bool hits_normalizer_extension::is_builtin(environment const & env, name const & n) const {
+    return is_hits_decl(env, n);
+}
+
 bool is_hits_decl(environment const & env, name const & n) {
     if (!get_extension(env).m_initialized)
         return false;
diff --git a/src/kernel/hits/hits.h b/src/kernel/hits/hits.h
index 05eecbcfa..59475fba5 100644
--- a/src/kernel/hits/hits.h
+++ b/src/kernel/hits/hits.h
@@ -18,6 +18,7 @@ public:
     virtual optional<expr> is_stuck(expr const & e, extension_context & ctx) const;
     virtual bool supports(name const & feature) const;
     virtual bool is_recursor(environment const & env, name const & n) const;
+    virtual bool is_builtin(environment const & env, name const & n) const;
 };
 
 /** \brief The following function must be invoked to register the builtin HITs computation rules in the kernel. */
diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp
index 01108161c..4a5c4b1b8 100644
--- a/src/kernel/inductive/inductive.cpp
+++ b/src/kernel/inductive/inductive.cpp
@@ -957,6 +957,10 @@ bool inductive_normalizer_extension::is_recursor(environment const & env, name c
     return static_cast<bool>(is_elim_rule(env, n));
 }
 
+bool inductive_normalizer_extension::is_builtin(environment const & env, name const & n) const {
+    return is_inductive_decl(env, n) || is_elim_rule(env, n) || is_intro_rule(env, n);
+}
+
 template<typename Ctx>
 optional<expr> is_elim_meta_app_core(Ctx & ctx, expr const & e) {
     inductive_env_ext const & ext = get_extension(ctx.env());
diff --git a/src/kernel/inductive/inductive.h b/src/kernel/inductive/inductive.h
index dc9323c40..0430d407c 100644
--- a/src/kernel/inductive/inductive.h
+++ b/src/kernel/inductive/inductive.h
@@ -20,6 +20,7 @@ public:
     virtual optional<expr> is_stuck(expr const & e, extension_context & ctx) const;
     virtual bool supports(name const & feature) const;
     virtual bool is_recursor(environment const & env, name const & n) const;
+    virtual bool is_builtin(environment const & env, name const & n) const;
 };
 
 /** \brief Introduction rule */
diff --git a/src/kernel/normalizer_extension.cpp b/src/kernel/normalizer_extension.cpp
index a095b3678..6c134a63e 100644
--- a/src/kernel/normalizer_extension.cpp
+++ b/src/kernel/normalizer_extension.cpp
@@ -15,6 +15,7 @@ public:
     virtual optional<expr> is_stuck(expr const &, extension_context &) const { return none_expr(); }
     virtual bool supports(name const &) const { return false; }
     virtual bool is_recursor(environment const &, name const &) const { return false; }
+    virtual bool is_builtin(environment const &, name const &) const { return false; }
 };
 
 std::unique_ptr<normalizer_extension> mk_id_normalizer_extension() {
@@ -49,6 +50,10 @@ public:
     virtual bool is_recursor(environment const & env, name const & n) const {
         return m_ext1->is_recursor(env, n) || m_ext2->is_recursor(env, n);
     }
+
+    virtual bool is_builtin(environment const & env, name const & n) const {
+        return m_ext1->is_builtin(env, n) || m_ext2->is_builtin(env, n);
+    }
 };
 
 std::unique_ptr<normalizer_extension> compose(std::unique_ptr<normalizer_extension> && ext1, std::unique_ptr<normalizer_extension> && ext2) {
diff --git a/src/kernel/normalizer_extension.h b/src/kernel/normalizer_extension.h
index 92b388e2f..d05426fc3 100644
--- a/src/kernel/normalizer_extension.h
+++ b/src/kernel/normalizer_extension.h
@@ -26,6 +26,7 @@ public:
         this method is only used for sanity checking. */
     virtual bool supports(name const & feature) const = 0;
     virtual bool is_recursor(environment const & env, name const & n) const = 0;
+    virtual bool is_builtin(environment const & env, name const & n) const = 0;
 };
 
 inline optional<pair<expr, constraint_seq>> none_ecs() { return optional<pair<expr, constraint_seq>>(); }
diff --git a/src/kernel/quotient/quotient.cpp b/src/kernel/quotient/quotient.cpp
index a0382b8af..5b3f0046a 100644
--- a/src/kernel/quotient/quotient.cpp
+++ b/src/kernel/quotient/quotient.cpp
@@ -126,6 +126,10 @@ bool quotient_normalizer_extension::is_recursor(environment const &, name const
     return n == *g_quotient_lift || n == *g_quotient_ind;
 }
 
+bool quotient_normalizer_extension::is_builtin(environment const & env, name const & n) const {
+    return is_quotient_decl(env, n);
+}
+
 bool is_quotient_decl(environment const & env, name const & n) {
     if (!get_extension(env).m_initialized)
         return false;
diff --git a/src/kernel/quotient/quotient.h b/src/kernel/quotient/quotient.h
index fa885e7c8..21e53fbfe 100644
--- a/src/kernel/quotient/quotient.h
+++ b/src/kernel/quotient/quotient.h
@@ -16,6 +16,7 @@ public:
     virtual optional<expr> is_stuck(expr const & e, extension_context & ctx) const;
     virtual bool supports(name const & feature) const;
     virtual bool is_recursor(environment const & env, name const & n) const;
+    virtual bool is_builtin(environment const & env, name const & n) const;
 };
 
 /** \brief The following function must be invoked to register the quotient type computation rules in the kernel. */
diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp
index c021b2160..e5e0edf37 100644
--- a/src/tests/kernel/environment.cpp
+++ b/src/tests/kernel/environment.cpp
@@ -137,6 +137,7 @@ public:
     virtual optional<expr> is_stuck(expr const &, extension_context &) const { return none_expr(); }
     virtual bool supports(name const &) const { return false; }
     virtual bool is_recursor(environment const &, name const &) const { return false; }
+    virtual bool is_builtin(environment const &, name const &) const { return false; }
 };
 
 static void tst3() {