diff --git a/tests/lean/bad_pattern.lean.expected.out b/tests/lean/bad_pattern.lean.expected.out
index 05f0463ab..27145d1fe 100644
--- a/tests/lean/bad_pattern.lean.expected.out
+++ b/tests/lean/bad_pattern.lean.expected.out
@@ -2,13 +2,16 @@ bad_pattern.lean:9:33: error: invalid pattern hint, pattern hints must be applic
 theorem tst₀ [forward] : ∀ (x : ℕ), P x :=
 sorry
 (multi-)patterns:
+?M_1 : ℕ
 {P ?M_1}
 theorem tst₁ [forward] : ∀ (x : ℕ), (:P x:) :=
 sorry
 (multi-)patterns:
+?M_1 : ℕ
 {P ?M_1}
 theorem tst₃ [forward] : ∀ (x : ℕ), P (:id x:) :=
 sorry
 (multi-)patterns:
+?M_1 : ℕ
 {P ?M_1}
 bad_pattern.lean:20:0: error: pattern inference failed for [forward] annotation, (solution: provide pattern hints using the notation '(: t :)' )
diff --git a/tests/lean/pattern_bug1.lean.expected.out b/tests/lean/pattern_bug1.lean.expected.out
index 1964b92f5..66899cd7f 100644
--- a/tests/lean/pattern_bug1.lean.expected.out
+++ b/tests/lean/pattern_bug1.lean.expected.out
@@ -1,4 +1,5 @@
 definition H [forward] : ∀ (a : A), (:P a:) → Exists (R a) :=
 sorry
 (multi-)patterns:
+?M_1 : A
 {P ?M_1}
diff --git a/tests/lean/pattern_hint1.lean.expected.out b/tests/lean/pattern_hint1.lean.expected.out
index 5467f0b49..2679a2d88 100644
--- a/tests/lean/pattern_hint1.lean.expected.out
+++ b/tests/lean/pattern_hint1.lean.expected.out
@@ -1,13 +1,16 @@
 definition foo₁ [forward] : ∀ (x : ℕ), f x ∧ g x :=
 sorry
 (multi-)patterns:
+?M_1 : ℕ
 {f ?M_1}
 {g ?M_1}
 definition foo₂ [forward] : ∀ (x : ℕ), (:f x:) ∧ g x :=
 sorry
 (multi-)patterns:
+?M_1 : ℕ
 {f ?M_1}
 definition foo₃ [forward] : ∀ (x : ℕ), (:f (id x):) ∧ g x :=
 sorry
 (multi-)patterns:
+?M_1 : ℕ
 {f ?M_1}
diff --git a/tests/lean/redundant_pattern.lean.expected.out b/tests/lean/redundant_pattern.lean.expected.out
index 3ca6801de..535233e15 100644
--- a/tests/lean/redundant_pattern.lean.expected.out
+++ b/tests/lean/redundant_pattern.lean.expected.out
@@ -1,4 +1,5 @@
 definition foo [forward] : ∀ (m n k : ℕ), P (f m) → P (g n) → P (f k) → P k ∧ R (g m) (f n) ∧ P (g m) ∧ P (f n) :=
 λ (m n k : ℕ), sorry
 (multi-)patterns:
-{P ?M_1, R (g ?M_2) (f ?M_3)}
+?M_1 : ℕ, ?M_2 : ℕ, ?M_3 : ℕ
+{P ?M_3, R (g ?M_1) (f ?M_2)}