diff --git a/tests/lean/interactive/in4.input.expected.out b/tests/lean/interactive/in4.input.expected.out
index cd587b0db..e0ab2f797 100644
--- a/tests/lean/interactive/in4.input.expected.out
+++ b/tests/lean/interactive/in4.input.expected.out
@@ -7,10 +7,9 @@ rfl
 -- ACK
 -- ENDINFO
 -- AFTER REMOVE 8&9
--- BEGININFO
--- NAY
+-- BEGININFO STALE NAY
 -- ENDINFO
--- BEGININFO
+-- BEGININFO NAY
 -- ENDINFO
 -- BEGININFO
 -- TYPE|9|0