diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 589af1f8b7..60b73fc4c7 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -966,6 +966,10 @@ bool parser::parse_binder_collection(buffer<pair<pos_info, name>> const & names,
     notation::accepting const & acc = head(acc_lst);
     lean_assert(!acc.get_postponed());
     expr pred     = acc.get_expr();
+    auto k        = p.first.get_action().kind();
+    if (k == notation::action_kind::Skip ||
+        k == notation::action_kind::Ext)
+        return false;
     unsigned rbp  = p.first.get_action().rbp();
     next(); // consume tk
     expr S        = parse_expr(rbp);
diff --git a/tests/lean/1290.lean b/tests/lean/1290.lean
new file mode 100644
index 0000000000..325c8deea6
--- /dev/null
+++ b/tests/lean/1290.lean
@@ -0,0 +1,12 @@
+structure Category :=
+  (Obj : Type)
+  (Hom : Obj -> Obj -> Type)
+
+structure Isomorphism ( C: Category ) { A B : C^.Obj } :=
+  (morphism : C^.Hom A B)
+
+instance Isomorphism_coercion_to_morphism { C : Category } { A B C^.Obj } : has_coe (Isomorphism C A B) (C^.Hom A B) :=
+  (coe: Isomorphism.morphism)
+
+instance Isomorphism_coercion_to_morphism_fixed { C : Category } { A B : C^.Obj } : has_coe (Isomorphism C) (C^.Hom A B) :=
+{coe := Isomorphism.morphism}
diff --git a/tests/lean/1290.lean.expected.out b/tests/lean/1290.lean.expected.out
new file mode 100644
index 0000000000..de648fdf09
--- /dev/null
+++ b/tests/lean/1290.lean.expected.out
@@ -0,0 +1 @@
+1290.lean:8:66: error: invalid declaration, '}' expected