diff --git a/tests/lean/run/cases_bug.lean b/tests/lean/run/cases_bug.lean
index 6a13169883..4c942b5686 100644
--- a/tests/lean/run/cases_bug.lean
+++ b/tests/lean/run/cases_bug.lean
@@ -1,2 +1,2 @@
 theorem cast_heq₂ : ∀ {A B : Type} (H : A = B) (a : A), cast H a == a
-| A A (eq.refl A) a := heq_of_eq $ cast_eq _ _
+| A ⌞A⌟ (eq.refl ⌞A⌟) a := heq_of_eq $ cast_eq _ _
diff --git a/tests/lean/run/unreachable_cases.lean b/tests/lean/run/unreachable_cases.lean
index 661175fdfd..d895227e8e 100644
--- a/tests/lean/run/unreachable_cases.lean
+++ b/tests/lean/run/unreachable_cases.lean
@@ -7,13 +7,13 @@ inductive ifin : ℕ → Type -- inductively defined fin-type
 open ifin
 
 definition foo {N : Type} : Π{n : ℕ}, N → ifin n → (N × ifin n)
-| (succ k) n (fz k) := sorry
+| (succ k) n (fz ⌞k⌟) := sorry
 | (succ k) n (fs x) := sorry
 
 definition bar {N : Type} : Π{n : ℕ}, (N × ifin n) → (N × ifin n)
-| (succ k) (n, fz k) := sorry
+| (succ k) (n, fz ⌞k⌟) := sorry
 | (succ k) (n, fs x) := sorry
 
 definition bar2 {N : Type} : Π{n : ℕ}, (N × ifin n) → (N × ifin n)
-| (succ k) (n, fz k) := sorry
+| (succ k) (n, fz ⌞k⌟) := sorry
 | (succ k) (n, fs x) := sorry