diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index f15f9b6179..6af96a1e5b 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -240,9 +240,9 @@ def notElem [BEq α] (a : α) (as : List α) : Bool :=
 abbrev contains [BEq α] (as : List α) (a : α) : Bool :=
   elem a as
 
-inductive Mem : α → List α → Prop
-  | head (a : α) (as : List α) : Mem a (a::as)
-  | tail (a : α) {b : α} {as : List α} : Mem b as → Mem b (a::as)
+inductive Mem (a : α) : List α → Prop
+  | head (as : List α) : Mem a (a::as)
+  | tail (b : α) {as : List α} : Mem a as → Mem a (b::as)
 
 instance : Membership α (List α) where
   mem := Mem
diff --git a/tests/lean/run/dotNameIssue.lean b/tests/lean/run/dotNameIssue.lean
index df334dcacf..5198e509f9 100644
--- a/tests/lean/run/dotNameIssue.lean
+++ b/tests/lean/run/dotNameIssue.lean
@@ -1,7 +1,7 @@
 example : x ≠ y → x ∉ [y] :=
   fun hne hin =>
     match hin with
-    | .head _ _ => hne rfl
+    | .head _ => hne rfl
 
 example : x ≠ y → x ∉ [y] :=
-  fun hne (.head _ _) => hne rfl
+  fun hne (.head _) => hne rfl