diff --git a/tests/lean/local_notation_bug.lean.expected.out b/tests/lean/local_notation_bug.lean.expected.out
index 11cccf2b1f..f31ab4af0e 100644
--- a/tests/lean/local_notation_bug.lean.expected.out
+++ b/tests/lean/local_notation_bug.lean.expected.out
@@ -1,8 +1,14 @@
 f a b : A
 f a b : A
+expr ↣ _Fun : expr.app
 string ↣ name : mk_simple_name
 nat ↣ bool : foo
+expr ↣ [fun-class] : expr.app
+expr ↣ _Fun : expr.app
 string ↣ name : mk_simple_name
+expr ↣ [fun-class] : expr.app
 10 : ?M_1
 local_notation_bug.lean:22:8: error: invalid expression
+expr ↣ _Fun : expr.app
 string ↣ name : mk_simple_name
+expr ↣ [fun-class] : expr.app
diff --git a/tests/lean/pp_proofs_coercions.lean.expected.out b/tests/lean/pp_proofs_coercions.lean.expected.out
index f289322de4..5d4c6b4a1f 100644
--- a/tests/lean/pp_proofs_coercions.lean.expected.out
+++ b/tests/lean/pp_proofs_coercions.lean.expected.out
@@ -1,5 +1,7 @@
+expr ↣ _Fun : expr.app
 string ↣ name : mk_simple_name
 C ↣ _Fun : f
+expr ↣ [fun-class] : expr.app
 C ↣ [fun-class] : f
 c
 c trivial
diff --git a/tests/lean/sec2.lean.expected.out b/tests/lean/sec2.lean.expected.out
index 5cd5b6fee7..72fa383c01 100644
--- a/tests/lean/sec2.lean.expected.out
+++ b/tests/lean/sec2.lean.expected.out
@@ -1,5 +1,7 @@
+expr ↣ _Fun : expr.app
 string ↣ name : mk_simple_name
 A ↣ B : f
+expr ↣ [fun-class] : expr.app
 g a : B
 sec2.lean:13:6: error: type mismatch at application
   g a
@@ -9,7 +11,9 @@ has type
   A
 but is expected to have type
   B
+expr ↣ _Fun : expr.app
 string ↣ name : mk_simple_name
 A ↣ B : f
+expr ↣ [fun-class] : expr.app
 g a : B
 g a : B