diff --git a/tests/lean/implicit4.lean.expected.out b/tests/lean/implicit4.lean.expected.out
index dfaa28674..26670ed9c 100644
--- a/tests/lean/implicit4.lean.expected.out
+++ b/tests/lean/implicit4.lean.expected.out
@@ -4,3 +4,8 @@
   Assumed: g
   Assumed: p
   Assumed: h
+The denotation(s) for the existing notation:
+  Infix ++
+have been replaced with the new denotation:
+  h::explicit
+because they conflict on how implicit arguments are used.
diff --git a/tests/lean/implicit5.lean.expected.out b/tests/lean/implicit5.lean.expected.out
index 4abcbeb39..8e1d9eb32 100644
--- a/tests/lean/implicit5.lean.expected.out
+++ b/tests/lean/implicit5.lean.expected.out
@@ -5,3 +5,8 @@
   Assumed: h
   Assumed: p
   Assumed: p2
+The denotation(s) for the existing notation:
+  Infix ++
+have been replaced with the new denotation:
+  p2::explicit
+because they conflict on how implicit arguments are used.
diff --git a/tests/lean/mod1.lean.expected.out b/tests/lean/mod1.lean.expected.out
index 166fcc2ba..9aa34a013 100644
--- a/tests/lean/mod1.lean.expected.out
+++ b/tests/lean/mod1.lean.expected.out
@@ -3,9 +3,11 @@
 Importing file 'simple.lean'
   Assumed: x
   Assumed: y
+Module 'simple.lean' has already been imported
 Importing file 'simple.lean'
   Assumed: x
   Assumed: y
+Module 'simple.lean' has already been imported
 x + y : ℤ
   Assumed: z
 z : ℤ
diff --git a/tests/lean/tactic6.lean.expected.out b/tests/lean/tactic6.lean.expected.out
index 3b672e2b9..7971625b0 100644
--- a/tests/lean/tactic6.lean.expected.out
+++ b/tests/lean/tactic6.lean.expected.out
@@ -1,4 +1,19 @@
   Set: pp::colors
   Set: pp::unicode
+Proof state:
+H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ a ∧ b
+Proof state:
+H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ a
+H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ b
   Proved: T
+Proof state:
+H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ c
+H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ a ∧ b
+Proof state:
+H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ a ∧ b
+Proof state:
+H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ c
+H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ b
+Proof state:
+H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ b
   Proved: T2
diff --git a/tests/lean/test.sh b/tests/lean/test.sh
index dd389bbd6..aaa4e4ad6 100755
--- a/tests/lean/test.sh
+++ b/tests/lean/test.sh
@@ -13,7 +13,7 @@ fi
 NUM_ERRORS=0
 for f in `ls *.lean`; do
     echo "-- testing $f"
-    $LEAN config.lean $f > $f.produced.out
+    $LEAN config.lean $f &> $f.produced.out
     if test -f $f.expected.out; then
         if diff $f.produced.out $f.expected.out; then
             echo "-- checked"
diff --git a/tests/lean/test_single.sh b/tests/lean/test_single.sh
index e9dd681c9..63837a6d1 100755
--- a/tests/lean/test_single.sh
+++ b/tests/lean/test_single.sh
@@ -12,7 +12,7 @@ else
 fi
 f=$2
 echo "-- testing $f"
-$LEAN config.lean $f > $f.produced.out
+$LEAN config.lean $f &> $f.produced.out
 if test -f $f.expected.out; then
     if diff $f.produced.out $f.expected.out; then
         echo "-- checked"