diff --git a/tests/lean/348.lean.expected.out b/tests/lean/348.lean.expected.out
index 4abed64a94..cedab7681d 100644
--- a/tests/lean/348.lean.expected.out
+++ b/tests/lean/348.lean.expected.out
@@ -1 +1,9 @@
 348.lean:3:24: error: expected ')'
+348.lean:2:2-2:47: error: application type mismatch
+  pure PUnit.unit
+argument
+  PUnit.unit
+has type
+  PUnit : Sort ?u
+but is expected to have type
+  String : Type
diff --git a/tests/lean/exitAfterParseError.lean.expected.out b/tests/lean/exitAfterParseError.lean.expected.out
index 87d0dd244a..3949f37412 100644
--- a/tests/lean/exitAfterParseError.lean.expected.out
+++ b/tests/lean/exitAfterParseError.lean.expected.out
@@ -1 +1,2 @@
-exitAfterParseError.lean:5:0: error: expected ':=', 'where' or '|'
+exitAfterParseError.lean:5:0: error: unexpected declaration body; expected ':=', 'where' or '|'
+exitAfterParseError.lean:3:0-3:7: error: declaration body is missing
diff --git a/tests/lean/tokenErrors.lean.expected.out b/tests/lean/tokenErrors.lean.expected.out
index 870f3972ca..c3d95dd62f 100644
--- a/tests/lean/tokenErrors.lean.expected.out
+++ b/tests/lean/tokenErrors.lean.expected.out
@@ -3,4 +3,10 @@ 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
+  failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)
 tokenErrors.lean:17:0: error: unterminated comment
+inductive Nat : Type
+constructors:
+Nat.zero : Nat
+Nat.succ : Nat → Nat
diff --git a/tests/lean/unknownTactic.lean.expected.out b/tests/lean/unknownTactic.lean.expected.out
index da22471d63..e9e743df06 100644
--- a/tests/lean/unknownTactic.lean.expected.out
+++ b/tests/lean/unknownTactic.lean.expected.out
@@ -1,5 +1,15 @@
 unknownTactic.lean:3:3: error: unknown tactic
+unknownTactic.lean:1:41-3:8: error: unsolved goals
+x : Nat
+a✝ : x = x
+⊢ x = x
 ---
 unknownTactic.lean:8:17: error: unknown tactic
+unknownTactic.lean:8:2-8:19: error: unsolved goals
+x : Nat
+⊢ x = x
 ---
 unknownTactic.lean:14:17: error: unknown tactic
+unknownTactic.lean:14:2-14:19: error: unsolved goals
+x : Nat
+⊢ x = x
diff --git a/tests/lean/weirdmacro.lean.expected.out b/tests/lean/weirdmacro.lean.expected.out
index ab28885346..e3dc899952 100644
--- a/tests/lean/weirdmacro.lean.expected.out
+++ b/tests/lean/weirdmacro.lean.expected.out
@@ -1,4 +1,6 @@
 weirdmacro.lean:1:6: error: expected no space before ':' or string literal
+weirdmacro.lean:1:0-1:5: error: unexpected syntax
+  failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)
 weirdmacro.lean:1:30-1:32: error: elaboration function for 'antiquot' has not been implemented
 weirdmacro.lean:1:32: error: expected command
 weirdmacro.lean:3:7-3:11: error: unknown identifier 'term'