diff --git a/tests/lean/interactive/completion.lean b/tests/lean/interactive/completion.lean
index defab7a739..ac77f755ee 100644
--- a/tests/lean/interactive/completion.lean
+++ b/tests/lean/interactive/completion.lean
@@ -3,15 +3,9 @@ structure Foo where
 
 example (f : Foo) : f.
                     --^ textDocument/completion
-example : Nat := 0  -- recover
-
 example (f : Foo) : f.f
                      --^ textDocument/completion
-example : Nat := 0  -- recover
-
 example (f : Foo) : id f |>.
                           --^ textDocument/completion
-example : Nat := 0  -- recover
-
 example (f : Foo) : id f |>.f
                            --^ textDocument/completion
diff --git a/tests/lean/interactive/completion.lean.expected.out b/tests/lean/interactive/completion.lean.expected.out
index bc5c33e059..671ed4ed66 100644
--- a/tests/lean/interactive/completion.lean.expected.out
+++ b/tests/lean/interactive/completion.lean.expected.out
@@ -5,19 +5,19 @@
   {"label": "mk", "detail": "Nat → Foo"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completion.lean"},
- "position": {"line": 7, "character": 23}}
+ "position": {"line": 5, "character": 23}}
 {"items":
  [{"label": "foo", "detail": "Foo → Nat"},
   {"label": "mk", "detail": "Nat → Foo"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completion.lean"},
- "position": {"line": 11, "character": 28}}
+ "position": {"line": 7, "character": 28}}
 {"items":
  [{"label": "foo", "detail": "Foo → Nat"},
   {"label": "mk", "detail": "Nat → Foo"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completion.lean"},
- "position": {"line": 15, "character": 29}}
+ "position": {"line": 9, "character": 29}}
 {"items":
  [{"label": "foo", "detail": "Foo → Nat"},
   {"label": "mk", "detail": "Nat → Foo"}],
diff --git a/tests/lean/tokenErrors.lean b/tests/lean/tokenErrors.lean
index e68d4c4d7c..8a20c89612 100644
--- a/tests/lean/tokenErrors.lean
+++ b/tests/lean/tokenErrors.lean
@@ -1,17 +1,7 @@
 #check 'hi
-example : Nat := 0  -- recover
-
 #check '\y'
-example : Nat := 0  -- recover
-
 #check "hi
-example : Nat := 0  -- recover
-
 #check hi.«
-example : Nat := 0  -- recover
-
 /--
-example : Nat := 0  -- recover
-
 #print Nat
 /-
diff --git a/tests/lean/tokenErrors.lean.expected.out b/tests/lean/tokenErrors.lean.expected.out
index b832ef295e..362fbce916 100644
--- a/tests/lean/tokenErrors.lean.expected.out
+++ b/tests/lean/tokenErrors.lean.expected.out
@@ -1,15 +1,15 @@
 tokenErrors.lean:1:10: error: missing end of character literal
-tokenErrors.lean:4:9: error: invalid escape sequence
-tokenErrors.lean:7:7: error: unterminated string literal
-tokenErrors.lean:10:11: error: unterminated identifier escape
-tokenErrors.lean:14:0: error: unterminated comment
-tokenErrors.lean:13:0-13:3: error: unexpected doc string
+tokenErrors.lean:2:9: error: invalid escape sequence
+tokenErrors.lean:3:7: error: unterminated string literal
+tokenErrors.lean:4:11: error: unterminated identifier escape
+tokenErrors.lean:6:0: error: unterminated comment
+tokenErrors.lean:5:0-5:3: error: unexpected doc string
   failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)
-tokenErrors.lean:17:0: error: unterminated comment
-tokenErrors.lean:16:0-16:6: error: unknown constant '[anonymous]'
+tokenErrors.lean:7:0: error: unterminated comment
+tokenErrors.lean:6:0-6:6: error: unknown constant '[anonymous]'
 inductive Nat : Type
 constructors:
 Nat.zero : Nat
 Nat.succ : Nat → Nat
-tokenErrors.lean:17:1: error: unterminated comment
-tokenErrors.lean:17:0-17:1: error: unexpected command
+tokenErrors.lean:7:1: error: unterminated comment
+tokenErrors.lean:7:0-7:1: error: unexpected command