diff --git a/tests/lean/appParserIssue.lean b/tests/lean/appParserIssue.lean
index 4bbdc9335e..13b145d7ee 100644
--- a/tests/lean/appParserIssue.lean
+++ b/tests/lean/appParserIssue.lean
@@ -9,5 +9,5 @@ new_frontend
 syntax "foo" term:max term:max : term
 macro_rules `(foo $x $y) => `(f $x $y)
 
-#check foo 1 fun x => x   -- should fail?
 #check foo 1 (fun x => x) -- should work
+#check foo 1 fun x => x   -- should fail?
diff --git a/tests/lean/appParserIssue.lean.expected.out b/tests/lean/appParserIssue.lean.expected.out
index 179073db77..8912a7bf7c 100644
--- a/tests/lean/appParserIssue.lean.expected.out
+++ b/tests/lean/appParserIssue.lean.expected.out
@@ -2,5 +2,4 @@ f 1 : (Nat → Nat) → Nat
 appParserIssue.lean:5:11: error: expected command
 f 1 (λ (x : Nat), x) : Nat
 f 1 (λ (x : Nat), x) : Nat
-appParserIssue.lean:12:13: error: unexpected token at this precedence level; consider parenthesizing the term
-f 1 (λ (x : Nat), x) : Nat
+appParserIssue.lean:13:13: error: unexpected token at this precedence level; consider parenthesizing the term
diff --git a/tests/lean/precissues.lean b/tests/lean/precissues.lean
index b2bd418e12..26b2127b7a 100644
--- a/tests/lean/precissues.lean
+++ b/tests/lean/precissues.lean
@@ -2,10 +2,14 @@ new_frontend
 
 #check id fun x => x -- should fail
 
+#check 0
+
 def f (x : Nat) (g : Nat → Nat) := g x
 
 #check f 1 fun x => x -- should fail
 
+#check 0
+
 #check f 1 (fun x => x)
 
 #check id have True from ⟨⟩; this -- should fail
diff --git a/tests/lean/precissues.lean.expected.out b/tests/lean/precissues.lean.expected.out
index 6ff08efadc..0ccbb1a762 100644
--- a/tests/lean/precissues.lean.expected.out
+++ b/tests/lean/precissues.lean.expected.out
@@ -1,11 +1,10 @@
 id : ?m_1 → ?m_1
 precissues.lean:3:10: error: expected command
 f 1 : (Nat → Nat) → Nat
-precissues.lean:7:11: error: expected command
+precissues.lean:9:11: error: expected command
 f 1 (λ (x : Nat), x) : Nat
 id : ?m_1 → ?m_1
-precissues.lean:11:10: error: expected command
-1 : Nat
+precissues.lean:15:10: error: expected command
 id ((λ (this : True), this) True.intro) : True
 0=(λ (this : Nat), this) 1 : Prop
 0=let x : Nat := 0 in x : Prop
diff --git a/tests/lean/run/macro.lean b/tests/lean/run/macro.lean
index a908175458..1cf032f830 100644
--- a/tests/lean/run/macro.lean
+++ b/tests/lean/run/macro.lean
@@ -6,7 +6,7 @@ axiom mem {α : Type} : α → Set α → Prop
 axiom univ {α : Type} : Set α
 axiom Union {α : Type} : Set (Set α) → Set α
 
-syntax term " ∈ ":100 term:99 : term
+syntax:100 term " ∈ " term:99 : term
 
 macro_rules
 | `($x ∈ $s) => `(mem $x $s)
diff --git a/tests/lean/run/termParserAttr.lean b/tests/lean/run/termParserAttr.lean
index 015ceaa66a..ae030c7911 100644
--- a/tests/lean/run/termParserAttr.lean
+++ b/tests/lean/run/termParserAttr.lean
@@ -13,7 +13,7 @@ do env  ← MetaIO.getEnv;
 
 open Lean.Parser
 
-@[termParser] def tst := parser! "(|" >> termParser >> optional (symbolAux ", " >> termParser) >> "|)"
+@[termParser] def tst := parser! "(|" >> termParser >> optional (symbol ", " >> termParser) >> "|)"
 
 @[termParser] def boo : ParserDescr :=
 ParserDescr.node `boo