diff --git a/src/library/blast/forward/pattern.cpp b/src/library/blast/forward/pattern.cpp
index a6710103ba..cc32f3266a 100644
--- a/src/library/blast/forward/pattern.cpp
+++ b/src/library/blast/forward/pattern.cpp
@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
 #include "library/kernel_serializer.h"
+#include "library/generic_exception.h"
 #include "library/tmp_type_context.h"
 #include "library/annotation.h"
 #include "library/occurs.h"
@@ -137,6 +138,8 @@ bool has_pattern_hints(expr const & e) {
 expr mk_pattern_hint(expr const & e) {
     if (has_pattern_hints(e))
         throw exception("invalid pattern hint, nested patterns hints are not allowed");
+    if (!is_app(e))
+        throw_generic_exception("invalid pattern hint, pattern must be applications", e);
     return mk_annotation(*g_pattern_hint, e);
 }
 
diff --git a/tests/lean/bad_pattern.lean b/tests/lean/bad_pattern.lean
new file mode 100644
index 0000000000..e987464c5c
--- /dev/null
+++ b/tests/lean/bad_pattern.lean
@@ -0,0 +1,7 @@
+constant P : nat → Prop
+
+lemma tst₁ [forward] : ∀ x, (: P x :) := -- Fine
+sorry
+
+lemma tst₂ [forward] : ∀ x, P (: x :) := -- Error
+sorry
diff --git a/tests/lean/bad_pattern.lean.expected.out b/tests/lean/bad_pattern.lean.expected.out
new file mode 100644
index 0000000000..33c209d666
--- /dev/null
+++ b/tests/lean/bad_pattern.lean.expected.out
@@ -0,0 +1 @@
+bad_pattern.lean:6:33: error: invalid pattern hint, pattern must be applications