diff --git a/tests/lean/notation2.lean.expected.out b/tests/lean/notation2.lean.expected.out
index 87bbe382a5..d2f39b6311 100644
--- a/tests/lean/notation2.lean.expected.out
+++ b/tests/lean/notation2.lean.expected.out
@@ -1,3 +1,2 @@
-notation2.lean:2:0: warning: imported file uses 'sorry'
 1 :: 2 :: nil : list num
 1 :: 2 :: 3 :: 4 :: 5 :: nil : list num
diff --git a/tests/lean/notation3.lean.expected.out b/tests/lean/notation3.lean.expected.out
index 23662a4fc7..66caff64b7 100644
--- a/tests/lean/notation3.lean.expected.out
+++ b/tests/lean/notation3.lean.expected.out
@@ -1,4 +1,3 @@
-notation3.lean:2:0: warning: imported file uses 'sorry'
 [ a, b, b ] : list num
 (a, true, a = b, b) : num × Prop × Prop × num
 (a, b) : num × num
diff --git a/tests/lean/notation4.lean.expected.out b/tests/lean/notation4.lean.expected.out
index 33ced86456..d5a812e952 100644
--- a/tests/lean/notation4.lean.expected.out
+++ b/tests/lean/notation4.lean.expected.out
@@ -1,4 +1,3 @@
-notation4.lean:2:0: warning: imported file uses 'sorry'
 ∃ (A : Type₁) (x y : A), x = y : Prop
 ∃ (x : num), x = 0 : Prop
 Σ (x : num), x = 10 : Type₁