diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 16f4261937..a2db5ed4f8 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -3487,9 +3487,9 @@ static void instantiate_replacements(type_context & ctx, buffer<expr_pair> & rep
     }
 }
 
-optional<expr> type_context::mk_class_instance(expr const & type) {
+optional<expr> type_context::mk_class_instance(expr const & type, bool assign_regular_uvars) {
     scope S(*this);
-    flet<bool> set(m_assign_regular_uvars_in_tmp_mode, true);
+    flet<bool> set(m_assign_regular_uvars_in_tmp_mode, assign_regular_uvars);
     optional<expr> result;
     buffer<expr_pair> replacements;
     if (in_tmp_mode()) {
@@ -3528,7 +3528,15 @@ optional<expr> type_context::mk_subsingleton_instance(expr const & type) {
     }
     level lvl    = sort_level(Type);
     expr subsingleton = mk_app(mk_constant(get_subsingleton_name(), {lvl}), type);
-    auto r = mk_class_instance(subsingleton);
+    /* We disable universe metavariable assignment, because we don't want
+       to prove that is a subsingleton in this case. More specifically, we don't want
+       Given (A : Sort ?u) (a : A), we don't want to report that 'a' is a
+       subsingleton by assigning ?u := 0.
+
+       See issue #1487
+    */
+    bool assign_regular_uvars = false;
+    auto r = mk_class_instance(subsingleton, assign_regular_uvars);
     m_cache->m_subsingleton_cache.insert(mk_pair(type, r));
     return r;
 }
diff --git a/src/library/type_context.h b/src/library/type_context.h
index 5665f27a70..6a3be563d8 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -448,7 +448,7 @@ public:
     optional<expr> expand_macro(expr const & e);
 
     optional<name> is_class(expr const & type);
-    optional<expr> mk_class_instance(expr const & type);
+    optional<expr> mk_class_instance(expr const & type, bool assign_regular_uvars = true);
     optional<expr> mk_subsingleton_instance(expr const & type);
     /* Create type class instance in a different local context */
     optional<expr> mk_class_instance_at(local_context const & lctx, expr const & type);
diff --git a/tests/lean/1487.lean b/tests/lean/1487.lean
new file mode 100644
index 0000000000..4bbc1857bb
--- /dev/null
+++ b/tests/lean/1487.lean
@@ -0,0 +1,4 @@
+def ex (α : Sort _) (a b : α) : a = b :=
+begin [smt]
+  close  -- Should fail
+end
diff --git a/tests/lean/1487.lean.expected.out b/tests/lean/1487.lean.expected.out
new file mode 100644
index 0000000000..25521b858d
--- /dev/null
+++ b/tests/lean/1487.lean.expected.out
@@ -0,0 +1,5 @@
+1487.lean:3:2: error: smt_tactic.close failed
+state:
+α : Sort ?,
+a b : α
+⊢ a = b