diff --git a/tests/lean/holes.lean.expected.out b/tests/lean/holes.lean.expected.out
index f8d63fd063..ec59697465 100644
--- a/tests/lean/holes.lean.expected.out
+++ b/tests/lean/holes.lean.expected.out
@@ -1,15 +1,4 @@
 holes.lean:4:4-4:7: error: placeholders '_' cannot be used where a function is expected
-holes.lean:11:8-11:13: error: don't know how to synthesize placeholder
-context:
-case hole
-x : Nat
-y : Nat
-⊢ Nat
-holes.lean:11:4-11:5: error: don't know how to synthesize placeholder
-context:
-x : Nat
-y : Nat
-⊢ Nat
 holes.lean:10:15-10:18: error: don't know how to synthesize implicit argument
   @g Nat (?m x) x
 context:
@@ -20,6 +9,17 @@ holes.lean:10:9-10:12: error: don't know how to synthesize implicit argument
 context:
 x : Nat
 ⊢ Type
+holes.lean:11:4-11:5: error: don't know how to synthesize placeholder
+context:
+x : Nat
+y : Nat
+⊢ Nat
+holes.lean:11:8-11:13: error: don't know how to synthesize placeholder
+context:
+case hole
+x : Nat
+y : Nat
+⊢ Nat
 holes.lean:13:10-13:11: error: failed to infer binder type
 holes.lean:15:16-15:17: error: failed to infer binder type
 holes.lean:19:0-19:3: error: don't know how to synthesize implicit argument
diff --git a/tests/lean/linterUnusedVariables.lean.expected.out b/tests/lean/linterUnusedVariables.lean.expected.out
index 2391423ea9..d2e8b55a11 100644
--- a/tests/lean/linterUnusedVariables.lean.expected.out
+++ b/tests/lean/linterUnusedVariables.lean.expected.out
@@ -3,8 +3,8 @@ linterUnusedVariables.lean:17:6-17:7: warning: unused variable `y` [linter.unuse
 linterUnusedVariables.lean:22:8-22:9: warning: unused variable `x` [linter.unusedVariables]
 linterUnusedVariables.lean:29:2-29:3: warning: unused variable `x` [linter.unusedVariables]
 linterUnusedVariables.lean:34:5-34:6: warning: unused variable `x` [linter.unusedVariables]
-linterUnusedVariables.lean:39:5-39:6: warning: unused variable `x` [linter.unusedVariables]
 linterUnusedVariables.lean:39:2-39:3: warning: unused variable `f` [linter.unusedVariables]
+linterUnusedVariables.lean:39:5-39:6: warning: unused variable `x` [linter.unusedVariables]
 linterUnusedVariables.lean:42:7-42:8: warning: unused variable `x` [linter.unusedVariables]
 linterUnusedVariables.lean:45:8-45:9: warning: unused variable `x` [linter.unusedVariables]
 linterUnusedVariables.lean:49:9-49:10: warning: unused variable `z` [linter.unusedVariables]
diff --git a/tests/lean/run/simp1.lean b/tests/lean/run/simp1.lean
index 559bf93981..88604e2257 100644
--- a/tests/lean/run/simp1.lean
+++ b/tests/lean/run/simp1.lean
@@ -29,6 +29,8 @@ axiom aux {α} (f : List α → List α) (xs ys : List α) : f (xs ++ ys) ++ []
 open Lean
 open Lean.Meta
 
+#eval 1 -- TODO: remove, this is a workaround to make sure then next eval works.
+
 def tst1 : MetaM Unit := do
   let thms  ← Meta.getSimpTheorems
   trace[Meta.debug] "{thms.pre}\n-----\n{thms.post}"