diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 3d26bc852e..b0bebd46c2 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -2213,9 +2213,10 @@ returns `a` if `opt = some a` and `dflt` otherwise.
 This function is `@[macro_inline]`, so `dflt` will not be evaluated unless
 `opt` turns out to be `none`.
 -/
-@[macro_inline] def Option.getD : Option α → α → α
-  | some x, _ => x
-  | none,   e => e
+@[macro_inline] def Option.getD (opt : Option α) (dflt : α) : α :=
+  match opt with
+  | some x => x
+  | none => dflt
 
 /--
 Map a function over an `Option` by applying the function to the contained
diff --git a/tests/lean/optionGetD.lean b/tests/lean/optionGetD.lean
new file mode 100644
index 0000000000..e32e15a15a
--- /dev/null
+++ b/tests/lean/optionGetD.lean
@@ -0,0 +1,12 @@
+import Lean.Data.HashMap
+
+def test (m : Lean.HashMap Nat Nat) : IO (Nat × Nat) := do
+  let start := 1
+  let mut i := start
+  let mut count := 0
+  while i != 0 do
+    i := (m.find? i).getD (panic! "key is not in the map")
+    count := count + 1
+  return (i, count)
+
+#eval test (.ofList [(1,3),(3,2),(2,0)])
diff --git a/tests/lean/optionGetD.lean.expected.out b/tests/lean/optionGetD.lean.expected.out
new file mode 100644
index 0000000000..3947600ce8
--- /dev/null
+++ b/tests/lean/optionGetD.lean.expected.out
@@ -0,0 +1 @@
+(0, 3)
diff --git a/tests/lean/smartUnfoldingMatch.lean.expected.out b/tests/lean/smartUnfoldingMatch.lean.expected.out
index 3d995b176e..2532b3c9eb 100644
--- a/tests/lean/smartUnfoldingMatch.lean.expected.out
+++ b/tests/lean/smartUnfoldingMatch.lean.expected.out
@@ -1,4 +1,4 @@
 42
-[Meta.debug] r: match x, 0 with
-    | some x, x_1 => x
-    | none, e => e
+[Meta.debug] r: match x with
+    | some x => x
+    | none => 0