diff --git a/library/data/quotient/basic.lean b/library/data/quotient/basic.lean
index 65f68d846..cd8830701 100644
--- a/library/data/quotient/basic.lean
+++ b/library/data/quotient/basic.lean
@@ -281,7 +281,7 @@ idempotent_image_fix (representative_map_idempotent H1 H2) b
 
 theorem representative_map_to_quotient {A : Type} {R : A → A → Prop} {f : A → A}
     (H1 : ∀a, R a (f a)) (H2 : ∀a a', R a a' ↔ R a a ∧ R a' a' ∧ f a = f a') :
-  is_quotient _ (fun_image f) elt_of :=
+  is_quotient R (fun_image f) elt_of :=
 let abs := fun_image f in
 intro
   (take u : image f,
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 882974cff..5ddc7aa7d 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -312,6 +312,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
         if (is_theorem) {
             auto type_pos = p.pos_of(type);
             std::tie(type, new_ls) = p.elaborate_type(type);
+            check_no_metavar(env, real_n, type, true);
             ls = append(ls, new_ls);
             expr type_as_is = p.save_pos(mk_as_is(type), type_pos);
             if (!p.collecting_info() && p.num_threads() > 1) {
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index c39c41cc2..481cc1006 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -421,7 +421,7 @@ type_checker::type_checker(environment const & env):
 
 type_checker::~type_checker() {}
 
-static void check_no_metavar(environment const & env, name const & n, expr const & e, bool is_type) {
+void check_no_metavar(environment const & env, name const & n, expr const & e, bool is_type) {
     if (has_metavar(e))
         throw_kernel_exception(env, e, [=](formatter const & fmt) { return pp_decl_has_metavars(fmt, n, e, is_type); });
 }
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index 82ee4098c..761b3bc51 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -204,6 +204,8 @@ public:
 
 typedef std::shared_ptr<type_checker> type_checker_ref;
 
+void check_no_metavar(environment const & env, name const & n, expr const & e, bool is_type);
+
 /**
    \brief Type check the given declaration, and return a certified declaration if it is type correct.
    Throw an exception if the declaration is type incorrect.