diff --git a/tests/lean/terminationFailure.lean b/tests/lean/terminationFailure.lean
index 197d23ef3696..bc2c7c00056a 100644
--- a/tests/lean/terminationFailure.lean
+++ b/tests/lean/terminationFailure.lean
@@ -8,8 +8,8 @@ where
   | 0 => 2
   | x => f x * 2
 
-#check! f
-#check! f.g
+#check f
+#check f.g
 
 #eval! f 0
 #eval! f.g 0
diff --git a/tests/lean/terminationFailure.lean.expected.out b/tests/lean/terminationFailure.lean.expected.out
index 48b6e3455b55..cc8cf7857550 100644
--- a/tests/lean/terminationFailure.lean.expected.out
+++ b/tests/lean/terminationFailure.lean.expected.out
@@ -19,25 +19,11 @@ Call from f to f.g at 3:4-7:
 x1 =
 
 Please use `termination_by` to specify a decreasing measure.
-terminationFailure.lean:11:8-11:9: error: application type mismatch
-  !f
-argument
-  f
-has type
-  Nat → Nat : Type
-but is expected to have type
-  Bool : Type
-!sorryAx Bool true : Bool
-terminationFailure.lean:12:8-12:11: error: application type mismatch
-  !f.g
-argument
-  f.g
-has type
-  Nat → Nat : Type
-but is expected to have type
-  Bool : Type
-!sorryAx Bool true : Bool
-terminationFailure.lean:22:4-22:5: error: fail to show termination for
+f (x : Nat) : Nat
+f.g : Nat → Nat
+1
+2
+terminationFailure.lean:20:4-20:5: error: fail to show termination for
   h
 with errors
 failed to infer structural recursion:
@@ -53,3 +39,4 @@ failed to prove termination, possible solutions:
 x : Nat
 ⊢ False
 h (x : Nat) : Foo
+Foo.a