diff --git a/tests/lean/nonexhaustive.lean.expected.out b/tests/lean/nonexhaustive.lean.expected.out
index 4d32e00b1..336f8a50c 100644
--- a/tests/lean/nonexhaustive.lean.expected.out
+++ b/tests/lean/nonexhaustive.lean.expected.out
@@ -1,4 +1,3 @@
-nonexhaustive.lean:2:0: warning: imported file uses 'sorry'
 nonexhaustive.lean:6:11: error: invalid non-exhaustive set of recursive equations, left-hand-side(s) after elaboration:
   @foo 0 (@nil A)
 
diff --git a/tests/lean/test.sh b/tests/lean/test.sh
index 35dfca742..2a0607802 100755
--- a/tests/lean/test.sh
+++ b/tests/lean/test.sh
@@ -15,7 +15,9 @@ fi
 NUM_ERRORS=0
 for f in *.lean; do
     echo "-- testing $f"
-    $LEAN -t config.lean $f &> $f.produced.out
+    $LEAN -t config.lean $f &> $f.produced.out.1
+    sed "/warning: imported file uses 'sorry'/d" $f.produced.out.1 > $f.produced.out
+    rm -f $f.produced.out.1
     if test -f $f.expected.out; then
         if diff -I "executing external script" $f.produced.out $f.expected.out; then
             echo "-- checked"
diff --git a/tests/lean/test_single.sh b/tests/lean/test_single.sh
index f33e6ff67..b2dce3ce8 100755
--- a/tests/lean/test_single.sh
+++ b/tests/lean/test_single.sh
@@ -13,7 +13,9 @@ else
 fi
 f=$2
 echo "-- testing $f"
-$LEAN config.lean $f &> $f.produced.out
+$LEAN config.lean $f &> $f.produced.out.1
+sed "/warning: imported file uses 'sorry'/d" $f.produced.out.1 > $f.produced.out
+rm -f $f.produced.out.1
 if test -f $f.expected.out; then
     if diff --ignore-all-space -I "executing external script" $f.produced.out $f.expected.out; then
         echo "-- checked"
diff --git a/tests/lean/unzip_error.lean.expected.out b/tests/lean/unzip_error.lean.expected.out
index d33d12844..a5d708bb4 100644
--- a/tests/lean/unzip_error.lean.expected.out
+++ b/tests/lean/unzip_error.lean.expected.out
@@ -1,3 +1,2 @@
-unzip_error.lean:2:0: warning: imported file uses 'sorry'
 unzip_error.lean:9:2: error: invalid recursive equation, left-hand-side contains meta-variable (possible solution: provide implicit parameters occurring in left-hand-side explicitly)
   match (@mk (vector A ?M_1) (vector B ?M_1) va vb)