diff --git a/tests/lean/interactive/in4.input.expected.out b/tests/lean/interactive/in4.input.expected.out
index f6146fdf9..679701599 100644
--- a/tests/lean/interactive/in4.input.expected.out
+++ b/tests/lean/interactive/in4.input.expected.out
@@ -14,5 +14,10 @@ rfl
 -- NAY
 -- ENDINFO
 -- BEGININFO
--- NAY
+-- TYPE|9|0
+∀ (a : A), eq a a
+-- ACK
+-- SYMBOL|9|0
+rfl
+-- ACK
 -- ENDINFO