diff --git a/src/library/scoped_ext.cpp b/src/library/scoped_ext.cpp
index c2d710065..62effe0e5 100644
--- a/src/library/scoped_ext.cpp
+++ b/src/library/scoped_ext.cpp
@@ -64,6 +64,14 @@ bool in_section(environment const & env) {
     return in_section_or_context(env) && !in_context(env);
 }
 
+void get_metaclasses(buffer<name> & r) {
+    for (auto const & t : get_exts()) {
+        name const & n = std::get<0>(t);
+        if (std::find(r.begin(), r.end(), n) == r.end())
+            r.push_back(n);
+    }
+}
+
 environment using_namespace(environment const & env, io_state const & ios, name const & n, name const & c) {
     environment r = env;
     for (auto const & t : get_exts()) {
diff --git a/src/library/scoped_ext.h b/src/library/scoped_ext.h
index ad000eb22..ba463c650 100644
--- a/src/library/scoped_ext.h
+++ b/src/library/scoped_ext.h
@@ -42,6 +42,9 @@ environment pop_scope_core(environment const & env);
 /** \brief Return true iff there are open scopes */
 bool has_open_scopes(environment const & env);
 
+/** \brief Store in \c r all metaobject classes available in Lean */
+void get_metaclasses(buffer<name> & r);
+
 /** \brief Add a new namespace (if it does not exist) */
 environment add_namespace(environment const & env, name const & ns);