diff --git a/src/Lean/Elab/Tactic/Match.lean b/src/Lean/Elab/Tactic/Match.lean
index 1444254784..8eddc607d2 100644
--- a/src/Lean/Elab/Tactic/Match.lean
+++ b/src/Lean/Elab/Tactic/Match.lean
@@ -63,7 +63,7 @@ private def mkAuxiliaryMatchTerm (parentTag : Name) (matchTac : Syntax) : MacroM
 def evalMatch : Tactic := fun stx => do
   let tag ← getMainTag
   let (matchTerm, cases) ← liftMacroM <| mkAuxiliaryMatchTerm tag stx
-  let refineMatchTerm ← `(tactic| refine $matchTerm)
+  let refineMatchTerm ← `(tactic| refine no_implicit_lambda% $matchTerm)
   let stxNew := mkNullNode (#[refineMatchTerm] ++ cases)
   withMacroExpansion stx stxNew <| evalTactic stxNew
 
diff --git a/tests/lean/995.lean b/tests/lean/995.lean
new file mode 100644
index 0000000000..e2d2cefe2a
--- /dev/null
+++ b/tests/lean/995.lean
@@ -0,0 +1,10 @@
+example : ∀(x : Nat){h : x = x}, Nat := by
+  intro x
+  match x with
+  | 0 => _
+  | n + 1 => _
+
+example (x : Nat) : ∀{h : x = x}, Nat := by
+  match x with
+  | 0 => _
+  | n + 1 => _
diff --git a/tests/lean/995.lean.expected.out b/tests/lean/995.lean.expected.out
new file mode 100644
index 0000000000..2a3fa30988
--- /dev/null
+++ b/tests/lean/995.lean.expected.out
@@ -0,0 +1,16 @@
+995.lean:1:40-5:14: error: unsolved goals
+case match_1
+x : Nat
+⊢ {h : 0 = 0} → Nat
+
+case match_2
+x n : Nat
+⊢ {h : n + 1 = n + 1} → Nat
+995.lean:7:41-10:14: error: unsolved goals
+case match_1
+x : Nat
+⊢ {h : 0 = 0} → Nat
+
+case match_2
+x n : Nat
+⊢ {h : n + 1 = n + 1} → Nat