diff --git a/src/library/blast/forward/pattern.cpp b/src/library/blast/forward/pattern.cpp
index c4d13e6fc..299b04755 100644
--- a/src/library/blast/forward/pattern.cpp
+++ b/src/library/blast/forward/pattern.cpp
@@ -550,9 +550,9 @@ struct mk_hi_lemma_fn {
         lean_assert(m_mvars.size() == inst_implicit_flags.size());
         buffer<expr> subst;
         buffer<expr> residue_locals;
+        candidate_set hints = collect_pattern_hints(m_mvars, B);
         expr proof  = mk_proof(residue_locals, subst);
         B           = replace_mvars(B, subst);
-        candidate_set hints = collect_pattern_hints(m_mvars, B);
         list<multi_pattern> mps;
         if (!hints.empty()) {
             mps = mk_multi_patterns_using(hints, false);
diff --git a/tests/lean/pattern_bug1.lean b/tests/lean/pattern_bug1.lean
new file mode 100644
index 000000000..dd64d91c1
--- /dev/null
+++ b/tests/lean/pattern_bug1.lean
@@ -0,0 +1,3 @@
+constants {A : Type} (P : A → Prop) (R : A → A → Prop)
+definition H [forward] : ∀ a, (: P a :) → ∃ b, R a b := sorry
+print H
diff --git a/tests/lean/pattern_bug1.lean.expected.out b/tests/lean/pattern_bug1.lean.expected.out
new file mode 100644
index 000000000..1964b92f5
--- /dev/null
+++ b/tests/lean/pattern_bug1.lean.expected.out
@@ -0,0 +1,4 @@
+definition H [forward] : ∀ (a : A), (:P a:) → Exists (R a) :=
+sorry
+(multi-)patterns:
+{P ?M_1}