diff --git a/tests/lean/bad_eqns.lean.expected.out b/tests/lean/bad_eqns.lean.expected.out
index 6abb0f294..0033c86e0 100644
--- a/tests/lean/bad_eqns.lean.expected.out
+++ b/tests/lean/bad_eqns.lean.expected.out
@@ -3,7 +3,7 @@ bad_eqns.lean:4:10: error: invalid argument, it is not a constructor, variable,
 in the following equation left-hand-side
   foo1 (0 + x)
 bad_eqns.lean:8:10: error: invalid equation left-hand-side, variable 'y' only occurs in inaccessible terms in the following equation left-hand-side
-  foo2 x y
+  foo2 x ⌞y⌟
 bad_eqns.lean:10:11: error: invalid recursive equations for 'foo3', inconsistent use of inaccessible term annotation, in some equations a pattern is a constructor, and in another it is an inaccessible term
 bad_eqns.lean:21:11: error: mutual recursion is not needed when defining non-recursive functions
 bad_eqns.lean:34:11: error: invalid recursive equations, failed to find recursive arguments that are structurally smaller (possible solution: use well-founded recursion)
diff --git a/tests/lean/error_loc_bug.lean.expected.out b/tests/lean/error_loc_bug.lean.expected.out
index 8b4b890f7..d904215c7 100644
--- a/tests/lean/error_loc_bug.lean.expected.out
+++ b/tests/lean/error_loc_bug.lean.expected.out
@@ -5,6 +5,6 @@ term
 has type
   Γ ⊢ A ∨ B
 but is expected to have type
-  Γ ⊢ A ∧ B
+  Γ ⊢ ⌞A ∧ B⌟
 The following identifier(s) are introduced as free variables by the left-hand-side of the equation:
   Γ A B Δ H Hs