diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 0607fbf884..0532b3fa34 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -390,7 +390,7 @@ private def expandMatchAltsIntoMatchAux (ref : Syntax) (matchAlts : Syntax) (mat
   if matchTactic then
     `(tactic| intro $x:term; $body:tactic)
   else
-    `(fun $x => $body)
+    `(@fun $x => $body)
 
 /--
   Expand `matchAlts` syntax into a full `match`-expression.
diff --git a/tests/lean/run/match1.lean b/tests/lean/run/match1.lean
index aae7cb8cd6..f84ebb440f 100644
--- a/tests/lean/run/match1.lean
+++ b/tests/lean/run/match1.lean
@@ -34,3 +34,27 @@ inductive C
 def C.x : C → Nat
 | C.mk₁ x   => x
 | C.mk₂ x _ => x
+
+def head : {α : Type} → List α → Option α
+| _, a::as => some a
+| _, _     => none
+
+theorem ex4 : head [1, 2] = some 1 :=
+rfl
+
+def head2 : {α : Type} → List α → Option α :=
+@fun
+  | _, a::as => some a
+  | _, _     => none
+
+theorem ex5 : head2 [1, 2] = some 1 :=
+rfl
+
+def head3 {α : Type} (xs : List α) : Option α :=
+let rec aux : {α : Type} → List α → Option α
+  | _, a::as => some a
+  | _, _     => none;
+aux xs
+
+theorem ex6 : head3 [1, 2] = some 1 :=
+rfl