diff --git a/tests/lean/531.hlean.expected.out b/tests/lean/531.hlean.expected.out
index 59c5ad3cd..c70917a50 100644
--- a/tests/lean/531.hlean.expected.out
+++ b/tests/lean/531.hlean.expected.out
@@ -1,7 +1 @@
-531.hlean:49:2: warning: using 'sorry'
-531.hlean:55:72: warning: using 'sorry'
-531.hlean:55:92: warning: using 'sorry'
-531.hlean:57:2: warning: using 'sorry'
-531.hlean:133:12: warning: using 'sorry'
-531.hlean:148:6: warning: using 'sorry'
 531.hlean:151:0: warning: using 'exit' to interrupt Lean
diff --git a/tests/lean/quot_bug.lean.expected.out b/tests/lean/quot_bug.lean.expected.out
index 13e60ba80..d925317ac 100644
--- a/tests/lean/quot_bug.lean.expected.out
+++ b/tests/lean/quot_bug.lean.expected.out
@@ -1,2 +1 @@
 λ (x : A), f x
-quot_bug.lean:8:59: warning: using 'sorry'
diff --git a/tests/lean/test_single.sh b/tests/lean/test_single.sh
index 91e7c0322..8bac28fed 100755
--- a/tests/lean/test_single.sh
+++ b/tests/lean/test_single.sh
@@ -22,7 +22,7 @@ fi
 
 echo "-- testing $f"
 "$LEAN" $CONFIG "$f" &> "$f.produced.out.1"
-sed "/warning: imported file uses 'sorry'/d" "$f.produced.out.1" > "$f.produced.out"
+sed "/warning: imported file uses 'sorry'/d" "$f.produced.out.1" | sed "/warning: using 'sorry'/d" > "$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