diff --git a/tests/lean/coe1.lean.expected.out b/tests/lean/coe1.lean.expected.out
index bc5249e4c7..c12964325d 100644
--- a/tests/lean/coe1.lean.expected.out
+++ b/tests/lean/coe1.lean.expected.out
@@ -1,4 +1,4 @@
-ite ↑tt "a" "b" : string
+ite ↥tt "a" "b" : string
 sine x : real
 sine ↑n : real
 sine ↑i : real
diff --git a/tests/lean/coe2.lean.expected.out b/tests/lean/coe2.lean.expected.out
index af71e818b8..0d9f349b97 100644
--- a/tests/lean/coe2.lean.expected.out
+++ b/tests/lean/coe2.lean.expected.out
@@ -1,4 +1,4 @@
-ite tt "a" "b" : string
+ite ↥tt "a" "b" : string
 sine x : real
 sine n : real
 sine i : real
diff --git a/tests/lean/no_coe.lean.expected.out b/tests/lean/no_coe.lean.expected.out
index bd6ffb145d..d6cc003bd8 100644
--- a/tests/lean/no_coe.lean.expected.out
+++ b/tests/lean/no_coe.lean.expected.out
@@ -1,4 +1,4 @@
-ite ↑tt 1 0 : ℕ
+ite ↥tt 1 0 : ℕ
 no_coe.lean:5:7: error: type mismatch at application
   ite tt
 term
diff --git a/tests/lean/print_meta.lean.expected.out b/tests/lean/print_meta.lean.expected.out
index 54e150f8d0..bf12d5cba3 100644
--- a/tests/lean/print_meta.lean.expected.out
+++ b/tests/lean/print_meta.lean.expected.out
@@ -2,4 +2,4 @@ meta def tactic.intro : name → tactic expr :=
 λ (n : name),
   tactic.target >>=
     λ (t : expr),
-      ite (↑(expr.is_pi t) ∨ ↑(expr.is_let t)) (tactic.intro_core n) (tactic.whnf_target >> tactic.intro_core n)
+      ite (↥(expr.is_pi t) ∨ ↥(expr.is_let t)) (tactic.intro_core n) (tactic.whnf_target >> tactic.intro_core n)