diff --git a/library/data/vector.lean b/library/data/vector.lean
index 6d9546ec25..734129cf4a 100644
--- a/library/data/vector.lean
+++ b/library/data/vector.lean
@@ -90,7 +90,7 @@ section accum
 end accum
 
 protected lemma eq {n : ℕ} : ∀ (a1 a2 : vector α n), to_list a1 = to_list a2 → a1 = a2
-| ⟨x, h1⟩ ⟨.x, h2⟩ rfl := rfl
+| ⟨x, h1⟩ ⟨._, h2⟩ rfl := rfl
 
 @[simp] lemma to_list_mk (v : list α) (P : list.length v = n) : to_list (subtype.mk v P) = v :=
 rfl
diff --git a/library/init/data/fin/basic.lean b/library/init/data/fin/basic.lean
index 333c0c6224..0809bd1a8c 100644
--- a/library/init/data/fin/basic.lean
+++ b/library/init/data/fin/basic.lean
@@ -16,10 +16,10 @@ def {u} elim0 {α : Type u} : fin 0 → α
 variable {n : nat}
 
 lemma eq_of_veq : ∀ {i j : fin n}, (val i) = (val j) → i = j
-| ⟨iv, ilt₁⟩ ⟨.iv, ilt₂⟩ rfl := rfl
+| ⟨iv, ilt₁⟩ ⟨.(iv), ilt₂⟩ rfl := rfl
 
 lemma veq_of_eq : ∀ {i j : fin n}, i = j → (val i) = (val j)
-| ⟨iv, ilt⟩ .⟨iv, ilt⟩ rfl := rfl
+| ⟨iv, ilt⟩ .(_) rfl := rfl
 
 lemma ne_of_vne {i j : fin n} (h : val i ≠ val j) : i ≠ j :=
 λ h', absurd (veq_of_eq h') h
diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean
index dd6ee7e1e3..4e527e33d0 100644
--- a/library/init/data/nat/lemmas.lean
+++ b/library/init/data/nat/lemmas.lean
@@ -287,8 +287,8 @@ lemma le_add_left (n m : ℕ): n ≤ m + n :=
 nat.add_comm n m ▸ le_add_right n m
 
 lemma le.dest : ∀ {n m : ℕ}, n ≤ m → ∃ k, n + k = m
-| n .n        (less_than_or_equal.refl .n)  := ⟨0, rfl⟩
-| n .(succ m) (@less_than_or_equal.step .n m h) :=
+| n ._ (less_than_or_equal.refl ._)  := ⟨0, rfl⟩
+| n ._ (@less_than_or_equal.step ._ m h) :=
   match le.dest h with
   | ⟨w, hw⟩ := ⟨succ w, hw ▸ add_succ n w⟩
   end
diff --git a/library/init/data/sigma/basic.lean b/library/init/data/sigma/basic.lean
index 7735f511b4..8603c52602 100644
--- a/library/init/data/sigma/basic.lean
+++ b/library/init/data/sigma/basic.lean
@@ -18,12 +18,12 @@ section
 variables {α : Type u} {β : α → Type v}
 
 protected lemma sigma.eq : ∀ {p₁ p₂ : Σ a : α, β a} (h₁ : p₁.1 = p₂.1), (eq.rec_on h₁ p₁.2 : β p₂.1) = p₂.2 → p₁ = p₂
-| ⟨a, b⟩ ⟨.a, .b⟩ rfl rfl := rfl
+| ⟨a, b⟩ ⟨.(a), .(b)⟩ rfl rfl := rfl
 end
 
 section
 variables {α : Sort u} {β : α → Sort v}
 
 protected lemma psigma.eq : ∀ {p₁ p₂ : psigma β} (h₁ : p₁.1 = p₂.1), (eq.rec_on h₁ p₁.2 : β p₂.1) = p₂.2 → p₁ = p₂
-| ⟨a, b⟩ ⟨.a, .b⟩ rfl rfl := rfl
+| ⟨a, b⟩ ⟨.(a), .(b)⟩ rfl rfl := rfl
 end
diff --git a/library/init/data/subtype/basic.lean b/library/init/data/subtype/basic.lean
index be0a766c35..69b0841ec6 100644
--- a/library/init/data/subtype/basic.lean
+++ b/library/init/data/subtype/basic.lean
@@ -20,7 +20,7 @@ lemma tag_irrelevant {a : α} (h1 h2 : p a) : mk a h1 = mk a h2 :=
 rfl
 
 protected lemma eq : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
-| ⟨x, h1⟩ ⟨.x, h2⟩ rfl := rfl
+| ⟨x, h1⟩ ⟨.(x), h2⟩ rfl := rfl
 
 end subtype
 
diff --git a/library/init/logic.lean b/library/init/logic.lean
index 55b4f0718e..56186bc2fe 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -163,13 +163,13 @@ heq.rec_on h (eq.refl α)
 end
 
 lemma eq_rec_heq {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} (h : a = a') (p : φ a), (eq.rec_on h p : φ a') == p
-| a .a rfl p := heq.refl p
+| a ._ rfl p := heq.refl p
 
 lemma heq_of_eq_rec_left {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a = a') (h₂ : (eq.rec_on e p₁ : φ a') = p₂), p₁ == p₂
-| a .a p₁ p₂ (eq.refl .a) h := eq.rec_on h (heq.refl p₁)
+| a ._ p₁ p₂ (eq.refl ._) h := eq.rec_on h (heq.refl p₁)
 
 lemma heq_of_eq_rec_right {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a' = a) (h₂ : p₁ = eq.rec_on e p₂), p₁ == p₂
-| a .a p₁ p₂ (eq.refl .a) h :=
+| a ._ p₁ p₂ (eq.refl ._) h :=
   have p₁ = p₂, from h,
   this ▸ heq.refl p₁
 
@@ -177,19 +177,19 @@ lemma of_heq_true {a : Prop} (h : a == true) : a :=
 of_eq_true (eq_of_heq h)
 
 lemma eq_rec_compose : ∀ {α β φ : Sort u} (p₁ : β = φ) (p₂ : α = β) (a : α), (eq.rec_on p₁ (eq.rec_on p₂ a : β) : φ) = eq.rec_on (eq.trans p₂ p₁) a
-| α .α .α (eq.refl .α) (eq.refl .α) a := rfl
+| α ._ ._ (eq.refl ._) (eq.refl ._) a := rfl
 
 lemma eq_rec_eq_eq_rec : ∀ {α₁ α₂ : Sort u} {p : α₁ = α₂} {a₁ : α₁} {a₂ : α₂}, (eq.rec_on p a₁ : α₂) = a₂ → a₁ = eq.rec_on (eq.symm p) a₂
-| α .α rfl a .a rfl := rfl
+| α ._ rfl a ._ rfl := rfl
 
 lemma eq_rec_of_heq_left : ∀ {α₁ α₂ : Sort u} {a₁ : α₁} {a₂ : α₂} (h : a₁ == a₂), (eq.rec_on (type_eq_of_heq h) a₁ : α₂) = a₂
-| α .α a .a (heq.refl .a) := rfl
+| α ._ a ._ (heq.refl ._) := rfl
 
 lemma eq_rec_of_heq_right {α₁ α₂ : Sort u} {a₁ : α₁} {a₂ : α₂} (h : a₁ == a₂) : a₁ = eq.rec_on (eq.symm (type_eq_of_heq h)) a₂ :=
 eq_rec_eq_eq_rec (eq_rec_of_heq_left h)
 
 lemma cast_heq : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a == a
-| α .α (eq.refl .α) a := heq.refl a
+| α ._ (eq.refl ._) a := heq.refl a
 
 /- and -/
 
diff --git a/library/init/meta/exceptional.lean b/library/init/meta/exceptional.lean
index 80134b6aff..6f6b0859db 100644
--- a/library/init/meta/exceptional.lean
+++ b/library/init/meta/exceptional.lean
@@ -20,7 +20,7 @@ variables [has_to_string α]
 
 protected meta def exceptional.to_string : exceptional α → string
 | (success a)       := to_string a
-| (exception .α e) := "Exception: " ++ to_string (e options.mk)
+| (exception .(α) e) := "Exception: " ++ to_string (e options.mk)
 
 meta instance : has_to_string (exceptional α) :=
 has_to_string.mk exceptional.to_string
@@ -31,11 +31,11 @@ variables {α β : Type}
 
 protected meta def to_bool : exceptional α → bool
 | (success _)      := tt
-| (exception .α _) := ff
+| (exception .(α) _) := ff
 
 protected meta def to_option : exceptional α → option α
 | (success a)      := some a
-| (exception .α _) := none
+| (exception .(α) _) := none
 
 @[inline] protected meta def bind (e₁ : exceptional α) (e₂ : α → exceptional β) : exceptional β :=
 exceptional.cases_on e₁
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 3d5a7e37af..ac6fb3e304 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -140,7 +140,7 @@ do o ← get_options,
 meta def returnex {α : Type} (e : exceptional α) : tactic α :=
 λ s, match e with
 | exceptional.success a      := success a s
-| exceptional.exception .α f :=
+| exceptional.exception ._ f :=
   match get_options s with
   | success opt _   := exception (some (λ u, f opt)) none s
   | exception _ _ _ := exception (some (λ u, f options.mk)) none s
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index b83a727acb..cb911b77ad 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -951,6 +951,20 @@ static expr parse_lambda_cons(parser_state & p, unsigned, expr const *, pos_info
     return p.save_pos(mk_choice(cs.size(), cs.data()), pos);
 }
 
+static expr parse_inaccessible(parser_state & p, unsigned, expr const *, pos_info const & pos) {
+    if (!p.in_pattern())
+        throw parser_error("inaccesible pattern notation `.(t)` can only be used in patterns", pos);
+    expr e = p.parse_expr();
+    p.check_token_next(get_rparen_tk(), "invalid inaccesible pattern, `)` expected");
+    return p.save_pos(mk_inaccessible(e), pos);
+}
+
+static expr parse_atomic_inaccessible(parser_state & p, unsigned, expr const *, pos_info const & pos) {
+    if (!p.in_pattern())
+        throw parser_error("inaccesible pattern notation `._` can only be used in patterns", pos);
+    return p.save_pos(mk_inaccessible(p.save_pos(mk_expr_placeholder(), pos)), pos);
+}
+
 parse_table init_nud_table() {
     action Expr(mk_expr_action());
     action Skip(mk_skip_action());
@@ -966,6 +980,8 @@ parse_table init_nud_table() {
     r = r.add({transition("(", mk_ext_action(parse_lparen))}, x0);
     r = r.add({transition("⟨", mk_ext_action(parse_constructor))}, x0);
     r = r.add({transition("{", mk_ext_action(parse_curly_bracket))}, x0);
+    r = r.add({transition(".(", mk_ext_action(parse_inaccessible))}, x0);
+    r = r.add({transition("._", mk_ext_action(parse_atomic_inaccessible))}, x0);
     r = r.add({transition("`(", mk_ext_action(parse_lazy_quoted_pexpr))}, x0);
     r = r.add({transition("``(", mk_ext_action(parse_quoted_pexpr))}, x0);
     r = r.add({transition("```(", mk_ext_action(parse_quoted_expr))}, x0);
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index ef38121cd9..33da943a1a 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1949,9 +1949,7 @@ expr parser::parse_char_expr() {
 expr parser::parse_nud() {
     switch (curr()) {
     case token_kind::Keyword:
-        if (m_in_pattern && curr_is_token(get_period_tk()))
-            return parse_inaccessible();
-        else if (curr_is_token(get_placeholder_tk()))
+        if (curr_is_token(get_placeholder_tk()))
             return parse_placeholder();
         else
             return parse_nud_notation();
@@ -1998,10 +1996,7 @@ expr parser::parse_led(expr left) {
 unsigned parser::curr_lbp() const {
     switch (curr()) {
     case token_kind::Keyword:
-        if (m_in_pattern && curr_is_token(get_period_tk()))
-            return get_max_prec();
-        else
-            return get_token_info().expr_precedence();
+        return get_token_info().expr_precedence();
     case token_kind::CommandKeyword: case token_kind::Eof:
     case token_kind::QuotedSymbol:   case token_kind::DocBlock:
     case token_kind::ModDocBlock:
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index c3b201f537..5ee580226c 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -87,7 +87,7 @@ void init_token_table(token_table & t) {
          {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0},
          {"Type", g_max_prec}, {"Type*", g_max_prec}, {"Sort", g_max_prec}, {"Sort*", g_max_prec},
-         {"(:", g_max_prec}, {":)", 0},
+         {"(:", g_max_prec}, {":)", 0}, {".(", g_max_prec}, {"._", g_max_prec},
          {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0},
          {"//", 0}, {"|", 0}, {"with", 0}, {"without", 0}, {"...", 0}, {",", 0},
          {".", 0}, {":", 0}, {"!", 0}, {"calc", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", g_max_prec},
diff --git a/tests/lean/bad_inaccessible.lean b/tests/lean/bad_inaccessible.lean
index b8f3602422..eabde01acb 100644
--- a/tests/lean/bad_inaccessible.lean
+++ b/tests/lean/bad_inaccessible.lean
@@ -1,9 +1,9 @@
 universe variables u
 definition f1 : nat → nat → nat
-| a .a := a
+| a .(a) := a
 
 definition f2 : ∀ (a b c : nat), a = c → c = a
-| a b .b rfl := rfl
+| a b .(b) rfl := rfl
 
 inductive vec (A : Type u) : nat → Type (max 1 u)
 | nil {}  : vec 0
diff --git a/tests/lean/bad_inaccessible.lean.expected.out b/tests/lean/bad_inaccessible.lean.expected.out
index 2bfa2331f3..67a4610e88 100644
--- a/tests/lean/bad_inaccessible.lean.expected.out
+++ b/tests/lean/bad_inaccessible.lean.expected.out
@@ -1,7 +1,7 @@
-bad_inaccessible.lean:3:5: error: invalid use of inaccessible term, it is not fixed by other arguments
-bad_inaccessible.lean:6:7: error: invalid use of inaccessible term, the provided term is
+bad_inaccessible.lean:3:6: error: invalid use of inaccessible term, it is not fixed by other arguments
+bad_inaccessible.lean:6:8: error: invalid use of inaccessible term, the provided term is
   b
 but is expected to be
   a
-bad_inaccessible.lean:14:3: error: invalid use of inaccessible term, it is not completely fixed by other arguments
+bad_inaccessible.lean:14:2: error: invalid use of inaccessible term, it is not completely fixed by other arguments
   .?m_1 + 1
diff --git a/tests/lean/bad_inaccessible2.lean b/tests/lean/bad_inaccessible2.lean
index f288ddeb14..ec97190b70 100644
--- a/tests/lean/bad_inaccessible2.lean
+++ b/tests/lean/bad_inaccessible2.lean
@@ -27,5 +27,5 @@ variables f : A → A → A
    3- Produce a better error message.
 -/
 definition map_head : ∀ {n}, vec A n → vec A n → vec A n
-| .0     nil nil                       := nil
-| .(n+1) (@cons .A .n a va) (@cons .A n b vb) := cons (f a b) va
+| .(0)     nil nil                       := nil
+| .(n+1) (@cons .(A) .(n) a va) (@cons .(A) n b vb) := cons (f a b) va
diff --git a/tests/lean/bad_inaccessible2.lean.expected.out b/tests/lean/bad_inaccessible2.lean.expected.out
index 4a7471c3be..40cb35ad2c 100644
--- a/tests/lean/bad_inaccessible2.lean.expected.out
+++ b/tests/lean/bad_inaccessible2.lean.expected.out
@@ -5,5 +5,5 @@ term
 has type
   vec .?m_1 (n + 1)
 but is expected to have type
-  vec A .(.?m_2 + 1)
-bad_inaccessible2.lean:31:46: error: ill-formed match/equations expression
+  vec A . (.?m_2 + 1)
+bad_inaccessible2.lean:31:52: error: ill-formed match/equations expression
diff --git a/tests/lean/def_inaccessible_issue.lean b/tests/lean/def_inaccessible_issue.lean
index 1671a7a870..361df887b4 100644
--- a/tests/lean/def_inaccessible_issue.lean
+++ b/tests/lean/def_inaccessible_issue.lean
@@ -12,6 +12,6 @@ variable (f : bool → bool → bool)
 
 definition map2 : ∀ {n}, bv n → bv n → bv n
 | 0     nil            nil             := nil
-| (n+1) (cons .n b1 v1) (cons .n b2 v2) := cons n (f b1 b2) (map2 v1 v2)
+| (n+1) (cons .(n) b1 v1) (cons .(n) b2 v2) := cons n (f b1 b2) (map2 v1 v2)
 
 #check map2.equations._eqn_2
diff --git a/tests/lean/eqn_compiler_error_msg.lean b/tests/lean/eqn_compiler_error_msg.lean
index 9e01986291..fb8c3758eb 100644
--- a/tests/lean/eqn_compiler_error_msg.lean
+++ b/tests/lean/eqn_compiler_error_msg.lean
@@ -2,4 +2,4 @@ inductive R : ℕ → Prop
 | pos : ∀p n, R (p + n)
 
 lemma R_id : ∀n, R n → R n
-| (.p + .n) (R.pos p n) := R.pos p n
+| (.(p) + .(n)) (R.pos p n) := R.pos p n
diff --git a/tests/lean/eqn_compiler_error_msg.lean.expected.out b/tests/lean/eqn_compiler_error_msg.lean.expected.out
index 4bf1bcea5d..87da101ec3 100644
--- a/tests/lean/eqn_compiler_error_msg.lean.expected.out
+++ b/tests/lean/eqn_compiler_error_msg.lean.expected.out
@@ -1,3 +1,3 @@
 eqn_compiler_error_msg.lean:5:2: error: invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )')
   .p + .n
-eqn_compiler_error_msg.lean:5:24: error: ill-formed match/equations expression
+eqn_compiler_error_msg.lean:5:28: error: ill-formed match/equations expression
diff --git a/tests/lean/inaccessible.lean b/tests/lean/inaccessible.lean
index 146fdaea7f..d06ce29d74 100644
--- a/tests/lean/inaccessible.lean
+++ b/tests/lean/inaccessible.lean
@@ -3,7 +3,7 @@ inductive imf {A : Type u} {B : Type v} (f : A → B) : B → Type (max 1 u v)
 | mk : ∀ (a : A), imf (f a)
 
 definition inv_1 {A : Type u} {B : Type v} (f : A → B) : ∀ (b : B), imf f b → A
-| .(f a) (imf.mk .f a)  := a
+| .(f a) (imf.mk .(f) a)  := a
 
 definition inv_2 {A : Type u} {B : Type v} (f : A → B) : ∀ (b : B), imf f b → A
 | ._ (imf.mk ._ a)  := a
@@ -14,7 +14,7 @@ definition inv_3 {A : Type u} {B : Type v} (f : A → B) : ∀ (b : B), imf f b
 | .(f a) (mk a)  := a -- Error, mk is not a constructor
 
 definition inv_4 {A : Type u} {B : Type v} (f : A → B) : ∀ (b : B), imf f b → A
-| .(f a) (.mk a)  := a -- Error, we cannot use inaccessible annotation around functions in applications
+| .(f a) (.(mk) a)  := a -- Error, we cannot use inaccessible annotation around functions in applications
 
 attribute [pattern] mk
 
@@ -44,8 +44,8 @@ section
 open vec1
 
 definition map_1 {A : Type u} (f : A → A → A) : Π {n}, vec1 A n → vec1 A n → vec1 A n
-| 0     (nil .A)        (nil .A)        := nil A
-| (n+1) (cons .n h₁ v₁) (cons .n h₂ v₂) := cons n (f h₁ h₂) (map_1 v₁ v₂)
+| 0     (nil .(A))        (nil .(A))        := nil A
+| (n+1) (cons .(n) h₁ v₁) (cons .(n) h₂ v₂) := cons n (f h₁ h₂) (map_1 v₁ v₂)
 
 definition map_2 {A : Type u} (f : A → A → A) : Π {n}, vec1 A n → vec1 A n → vec1 A n
 | 0     (nil ._)        (nil ._)        := nil A
@@ -54,7 +54,7 @@ definition map_2 {A : Type u} (f : A → A → A) : Π {n}, vec1 A n → vec1 A
 /- In map_3, we use the inaccessible terms to avoid pattern/matching on the first argument -/
 definition map_3 {A : Type u} (f : A → A → A) : Π {n}, vec1 A n → vec1 A n → vec1 A n
 | ._ (nil ._)      (nil ._)        := nil A
-| ._ (cons n h₁ v₁) (cons .n h₂ v₂) := cons n (f h₁ h₂) (map_3 v₁ v₂)
+| ._ (cons n h₁ v₁) (cons .(n) h₂ v₂) := cons n (f h₁ h₂) (map_3 v₁ v₂)
 end
 
 inductive vec2 (A : Type u) : nat → Type (max 1 u)
@@ -70,7 +70,7 @@ definition map_4 {A : Type u} (f : A → A → A) : Π {n}, vec2 A n → vec2 A
 
 definition map_5 {A : Type u} (f : A → A → A) : Π {n}, vec2 A n → vec2 A n → vec2 A n
 | ._  nil          nil         := nil
-| ._ (@cons .A n h₁ v₁) (cons h₂ v₂) := cons (f h₁ h₂) (map_5 v₁ v₂)
+| ._ (@cons ._ n h₁ v₁) (cons h₂ v₂) := cons (f h₁ h₂) (map_5 v₁ v₂)
 
 /-
 The following variant will be rejected by the new equation compiler.
diff --git a/tests/lean/inaccessible.lean.expected.out b/tests/lean/inaccessible.lean.expected.out
index e69c0c0ed9..0e3c7c92ce 100644
--- a/tests/lean/inaccessible.lean.expected.out
+++ b/tests/lean/inaccessible.lean.expected.out
@@ -3,7 +3,7 @@ inaccessible.lean:14:10: error: function expected at
 inaccessible.lean:14:2: error: invalid occurrence of macro expression in pattern (possible solution, mark term as inaccessible using '.( )')
   sorry
 inaccessible.lean:14:17: error: ill-formed match/equations expression
-inaccessible.lean:17:11: error: invalid inaccessible annotation, it cannot be used around functions in applications
+inaccessible.lean:17:12: error: invalid inaccessible annotation, it cannot be used around functions in applications
 inaccessible.lean:25:12: error: invalid pattern, 'a' already appeared in this pattern
 inaccessible.lean:28:3: error: function expected at
   f
@@ -17,5 +17,5 @@ but is expected to have type
   imf f sorry
 inaccessible.lean:28:16: error: ill-formed match/equations expression
 inaccessible.lean:31:4: error: invalid pattern, 'a' already appeared in this pattern
-inaccessible.lean:82:3: error: invalid use of inaccessible term, it is not completely fixed by other arguments
+inaccessible.lean:82:2: error: invalid use of inaccessible term, it is not completely fixed by other arguments
   .?m_1 + 1
diff --git a/tests/lean/inaccessible2.lean b/tests/lean/inaccessible2.lean
index 855153b722..eabd5f401f 100644
--- a/tests/lean/inaccessible2.lean
+++ b/tests/lean/inaccessible2.lean
@@ -2,13 +2,13 @@ inductive imf {A B : Sort*} (f : A → B) : B → Sort*
 | mk : ∀ (a : A), imf (f a)
 
 definition inv_1 {A B : Sort*} (f : A → B) : ∀ (b : B), imf f b → A
-| .(f .a) (imf.mk .f a)  := a  -- Error inaccessible annotation inside inaccessible annotation
+| .(f .(a)) (imf.mk .(f) a)  := a  -- Error inaccessible annotation inside inaccessible annotation
 
 definition inv_2 {A B : Sort*} (f : A → B) : ∀ (b : B), imf f b → A
-| .(f a) (let x := (imf.mk .f a) in x)  := a  -- Error invalid occurrence of 'let' expression
+| .(f a) (let x := (imf.mk .(f) a) in x)  := a  -- Error invalid occurrence of 'let' expression
 
 definition inv_3 {A B : Sort*} (f : A → B) : ∀ (b : B), imf f b → A
-| .(f a) ((λ (x : imf f b), x) (imf.mk .f a)) := a  -- Error invalid occurrence of 'lambda' expression
+| .(f a) ((λ (x : imf f b), x) (imf.mk .(f) a)) := a  -- Error invalid occurrence of 'lambda' expression
 
 definition symm {A : Sort*} : ∀ a b : A, a = b → b = a
-| .a .a (eq.refl a) := rfl -- Error `a` in eq.refl must be marked as inaccessible since it is an inductive datatype parameter
+| .(a) .(a) (eq.refl a) := rfl -- Error `a` in eq.refl must be marked as inaccessible since it is an inductive datatype parameter
diff --git a/tests/lean/inaccessible2.lean.expected.out b/tests/lean/inaccessible2.lean.expected.out
index 614ca5c89a..3aec02af02 100644
--- a/tests/lean/inaccessible2.lean.expected.out
+++ b/tests/lean/inaccessible2.lean.expected.out
@@ -1,9 +1,9 @@
-inaccessible2.lean:5:7: error: invalid occurrence of 'inaccessible' annotation, it must only occur in patterns
+inaccessible2.lean:5:8: error: invalid occurrence of 'inaccessible' annotation, it must only occur in patterns
 inaccessible2.lean:5:4: error: invalid use of inaccessible term, the provided term is
   f sorry
 but is expected to be
   f a
 inaccessible2.lean:8:10: error: invalid pattern, must be an application, constant, variable, type ascription or inaccessible term
-inaccessible2.lean:11:39: error: invalid expression, `)` expected
-inaccessible2.lean:14:9: error: invalid pattern, in a constructor application, the parameters of the inductive datatype must be marked as inaccessible
-inaccessible2.lean:14:20: error: ill-formed match/equations expression
+inaccessible2.lean:11:39: error: inaccesible pattern notation `.(t)` can only be used in patterns
+inaccessible2.lean:14:13: error: invalid pattern, in a constructor application, the parameters of the inductive datatype must be marked as inaccessible
+inaccessible2.lean:14:24: error: ill-formed match/equations expression
diff --git a/tests/lean/run/1163.lean b/tests/lean/run/1163.lean
index ee3374aa11..52837a2cdb 100644
--- a/tests/lean/run/1163.lean
+++ b/tests/lean/run/1163.lean
@@ -3,5 +3,5 @@ inductive {u} Foo : Type → Type (u+1)
 | wrap   : Π (X : Type), Foo X → Foo X
 
 def rig : Π {X : Type}, Foo X → Foo X
-| X (Foo.wrap .X foo)  := foo
-| X foo                := foo
+| X (Foo.wrap .(X) foo)  := foo
+| X foo                  := foo
diff --git a/tests/lean/run/1216.lean b/tests/lean/run/1216.lean
index d0db2c453c..1ff1260266 100644
--- a/tests/lean/run/1216.lean
+++ b/tests/lean/run/1216.lean
@@ -16,8 +16,8 @@ def get₂b {A : Type} : Π {n : ℕ}, Vec A (n+2) → A
 | n (cons x₁ (cons x₂ xs)) := x₂
 
 def get₂c {A : Type} : Π {n : ℕ}, Vec A (n+2) → A
-| .n (@cons .A x₁ .(n+1) (@cons .A x₂ n xs)) := x₂
+| .(n) (@cons .(A) x₁ .(n+1) (@cons .(A) x₂ n xs)) := x₂
 
 def get₂d {A : Type} : Π {n : ℕ}, Vec A (n+2) → A
-| .n (@cons .A x₁ (n+1) (@cons .A x₂ .n xs)) := x₂
+| .(n) (@cons .(A) x₁ (n+1) (@cons .(A) x₂ .(n) xs)) := x₂
 end Vec
diff --git a/tests/lean/run/662.lean b/tests/lean/run/662.lean
index c6a8689765..8e316f4781 100644
--- a/tests/lean/run/662.lean
+++ b/tests/lean/run/662.lean
@@ -28,8 +28,8 @@ definition count_vars : Π {t : type}, @term (λ x, unit) t -> nat
 | Nat        (Const x)              := 0
 | Nat        (Plus e1 e2)           := count_vars e1 + count_vars e2
 | (Func A B) (Abs e1)               := count_vars (e1 star)
-| B          (@App ._ A .B e1 e2)   := count_vars e1 + count_vars e2
-| B          (@Let ._ A .B e1 e2)   := count_vars e1 + count_vars (e2 star)
+| B          (@App ._ A .(B) e1 e2)   := count_vars e1 + count_vars e2
+| B          (@Let ._ A .(B) e1 e2)   := count_vars e1 + count_vars (e2 star)
 
 definition var (t : type) : @term (λ x, unit) t :=
 Var star
diff --git a/tests/lean/run/cases_bug.lean b/tests/lean/run/cases_bug.lean
index c50af39a00..a848ae9899 100644
--- a/tests/lean/run/cases_bug.lean
+++ b/tests/lean/run/cases_bug.lean
@@ -1,2 +1,2 @@
 theorem cast_heq₂ : ∀ {A B : Type} (H : A = B) (a : A), cast H a == a
-| A .A (eq.refl .A) a := heq_of_eq $ cast_eq _ _
+| A .(A) (eq.refl .(A)) a := heq_of_eq $ cast_eq _ _
diff --git a/tests/lean/run/cases_bug3.lean b/tests/lean/run/cases_bug3.lean
index f709594db0..c61fbe0a6a 100644
--- a/tests/lean/run/cases_bug3.lean
+++ b/tests/lean/run/cases_bug3.lean
@@ -1,3 +1,2 @@
-
 theorem ex {A : Type} : ∀ {a a' : A}, a == a' → a = a'
-| a .a (heq.refl .a) := eq.refl a
+| a .(a) (heq.refl .(a)) := eq.refl a
diff --git a/tests/lean/run/def10.lean b/tests/lean/run/def10.lean
index 86ff74ffff..ea254c6f0b 100644
--- a/tests/lean/run/def10.lean
+++ b/tests/lean/run/def10.lean
@@ -8,7 +8,7 @@ open bv bool
 
 definition h : ∀ {n}, bv (succ (succ n)) → bool
 | .(succ m) (cons (succ (succ m)) b v) := b
-| .0        (cons (succ nat.zero) b v) := bnot b
+| .(0)      (cons (succ nat.zero) b v) := bnot b
 
 example (m : nat) (b : bool) (v : bv (succ (succ m))) : @h (succ m) (cons (succ (succ m)) b v) = b :=
 rfl
diff --git a/tests/lean/run/def13.lean b/tests/lean/run/def13.lean
index 4901ecdee4..2358a60889 100644
--- a/tests/lean/run/def13.lean
+++ b/tests/lean/run/def13.lean
@@ -1,4 +1,3 @@
-
 inductive vec (A : Type) : nat → Type
 | nil {} : vec 0
 | cons   : Π {n}, A → vec n → vec (n+1)
@@ -9,8 +8,8 @@ variables {A : Type}
 variables f : A → A → A
 
 definition map_head_1 : ∀ {n}, vec A n → vec A n → vec A n
-| .0     nil nil                       := nil
-| .(n+1) (@cons .A n a va) (cons b vb) := cons (f a b) va
+| .(0)     nil nil                       := nil
+| .(n+1) (@cons .(A) n a va) (cons b vb) := cons (f a b) va
 
 example : map_head_1 f nil nil = nil :=
 rfl
diff --git a/tests/lean/run/def8.lean b/tests/lean/run/def8.lean
index a2692880cc..c9e59eac71 100644
--- a/tests/lean/run/def8.lean
+++ b/tests/lean/run/def8.lean
@@ -1,9 +1,8 @@
-
 inductive imf {A B : Type} (f : A → B) : B → Type
 | mk : ∀ (a : A), imf (f a)
 
 definition g {A B : Type} {f : A → B} : ∀ {b : B}, imf f b → A
-| .(f a) (imf.mk .f a)  := a
+| .(f a) (imf.mk .(f) a)  := a
 
 example {A B : Type} (f : A → B) (a : A) : g (imf.mk f a) = a :=
 rfl
@@ -21,10 +20,10 @@ example : g v₂ = 0 :=
 rfl
 
 lemma ex1 (A : Type) : ∀ (a b : A) (H : a = b), b = a
-| a .a rfl := rfl
+| a .(a) rfl := rfl
 
 lemma ex2 (A : Type) : ∀ a b : A, a = b → b = a
-| a .a (eq.refl .a) := rfl
+| a .(a) (eq.refl .(a)) := rfl
 
 lemma ex3 (A : Type) : ∀ a b : A, a = b → b = a
 | a ._ (eq.refl ._) := rfl
diff --git a/tests/lean/run/def9.lean b/tests/lean/run/def9.lean
index a05ac5068b..5a9652d832 100644
--- a/tests/lean/run/def9.lean
+++ b/tests/lean/run/def9.lean
@@ -1,3 +1,2 @@
-
 lemma ex4 (A : Type) : ∀ (a b : A) (H : a = b), b = a
-| .z z (eq.refl .z) := eq.refl z
+| .(z) z (eq.refl .(z)) := eq.refl z
diff --git a/tests/lean/run/def_brec1.lean b/tests/lean/run/def_brec1.lean
index 470e1550c9..578f3ad05b 100644
--- a/tests/lean/run/def_brec1.lean
+++ b/tests/lean/run/def_brec1.lean
@@ -1,4 +1,3 @@
-
 inductive foo : bool → Type
 | Z  : foo ff
 | O  : foo ff → foo tt
@@ -7,9 +6,9 @@ inductive foo : bool → Type
 open foo
 
 definition to_nat : ∀ {b}, foo b → nat
-| .ff Z     := 0
-| .tt (O n) := to_nat n + 1
-| .ff (E n) := to_nat n + 1
+| .(ff) Z     := 0
+| .(tt) (O n) := to_nat n + 1
+| .(ff) (E n) := to_nat n + 1
 
 example : to_nat (E (O Z)) = 2 :=
 rfl
diff --git a/tests/lean/run/def_brec3.lean b/tests/lean/run/def_brec3.lean
index 8621b27af7..30e8bba41c 100644
--- a/tests/lean/run/def_brec3.lean
+++ b/tests/lean/run/def_brec3.lean
@@ -9,8 +9,8 @@ open bv
 variable (f : bool → bool → bool)
 
 definition map2 : ∀ {n}, bv n → bv n → bv n
-| .0     nil            nil             := nil
-| .(n+1) (cons n b1 v1) (cons .n b2 v2) := cons n (f b1 b2) (map2 v1 v2)
+| .(0)     nil            nil             := nil
+| .(n+1) (cons n b1 v1) (cons .(n) b2 v2) := cons n (f b1 b2) (map2 v1 v2)
 
 example : map2 f nil nil = nil :=
 rfl
diff --git a/tests/lean/run/def_brec4.lean b/tests/lean/run/def_brec4.lean
index 957891c413..c5ad157abf 100644
--- a/tests/lean/run/def_brec4.lean
+++ b/tests/lean/run/def_brec4.lean
@@ -10,7 +10,7 @@ variable (f : bool → bool → bool)
 
 definition map2 : ∀ {n}, bv n → bv n → bv n
 | 0     nil            nil             := nil
-| (n+1) (cons .n b1 v1) (cons .n b2 v2) := cons n (f b1 b2) (map2 v1 v2)
+| (n+1) (cons .(n) b1 v1) (cons .(n) b2 v2) := cons n (f b1 b2) (map2 v1 v2)
 
 example : map2 f nil nil = nil :=
 rfl
diff --git a/tests/lean/run/def_ite_value.lean b/tests/lean/run/def_ite_value.lean
index f31c2362fa..6f8a089cf5 100644
--- a/tests/lean/run/def_ite_value.lean
+++ b/tests/lean/run/def_ite_value.lean
@@ -5,9 +5,9 @@ inductive bv : nat → Type
 open bv
 
 definition f : ∀ n : nat, bv n → nat → nat
-| (n+1) (cons .n b v) 1000000 := f n v 0
-| (n+1) (cons .n b v) x      := f n v (x + 1)
-| _     _             _      := 1
+| (n+1) (cons .(n) b v) 1000000 := f n v 0
+| (n+1) (cons .(n) b v) x       := f n v (x + 1)
+| _     _                _      := 1
 
 set_option pp.binder_types true
 
diff --git a/tests/lean/run/eq2.lean b/tests/lean/run/eq2.lean
index 266c3424d3..e56c577337 100644
--- a/tests/lean/run/eq2.lean
+++ b/tests/lean/run/eq2.lean
@@ -1,6 +1,5 @@
-
 definition symm {A : Type} : Π {a b : A}, a = b → b = a
-| a .a rfl := rfl
+| a .(a) rfl := rfl
 
 definition trans {A : Type} : Π {a b c : A}, a = b → b = c → a = c
-| a .a .a rfl rfl := rfl
+| a .(a) .(a) rfl rfl := rfl
diff --git a/tests/lean/run/eq9.lean b/tests/lean/run/eq9.lean
index cf427791b4..40f62820b3 100644
--- a/tests/lean/run/eq9.lean
+++ b/tests/lean/run/eq9.lean
@@ -3,5 +3,5 @@ attribute [pattern] lt.base
 attribute [pattern] lt.step
 
 theorem lt_succ {a : nat} : ∀ {b : nat}, a < b → succ a < succ b
-| .(succ a) (lt.base .a)       := lt.base (succ a)
-| .(succ b) (@lt.step .a b h)  := lt.step (lt_succ h)
+| .(succ a) (lt.base .(a))       := lt.base (succ a)
+| .(succ b) (@lt.step .(a) b h)  := lt.step (lt_succ h)
diff --git a/tests/lean/run/match2.lean b/tests/lean/run/match2.lean
index 8ef703405c..493a05216e 100644
--- a/tests/lean/run/match2.lean
+++ b/tests/lean/run/match2.lean
@@ -3,5 +3,5 @@ inductive imf (f : nat → nat) : nat → Type
 | mk2 : imf (f 0 + 1)
 
 definition inv_2 (f : nat → nat) : ∀ (b : nat), imf f b → {x : nat // x > b} → nat
-| .(f a)     (imf.mk1 .f a) x := a
-| .(f 0 + 1) (imf.mk2 .f)   x := subtype.val x
+| .(f a)     (imf.mk1 .(f) a) x := a
+| .(f 0 + 1) (imf.mk2 .(f))   x := subtype.val x
diff --git a/tests/lean/run/pack_unpack1.lean b/tests/lean/run/pack_unpack1.lean
index c5eb249d2d..01e3191c00 100644
--- a/tests/lean/run/pack_unpack1.lean
+++ b/tests/lean/run/pack_unpack1.lean
@@ -17,10 +17,10 @@ definition pack {A : Sort*} : list (tree A) → tree_core A tt
 | (a::l) := cons' a (pack l)
 
 definition unpack {A : Sort*} : ∀ {b}, tree_core A b → list (tree A)
-| .tt nil'         := []
-| .tt (cons' a t)  := a :: unpack t
-| .ff (leaf' a)    := []
-| .ff (node' l)    := []
+| .(tt) nil'         := []
+| .(tt) (cons' a t)  := a :: unpack t
+| .(ff) (leaf' a)    := []
+| .(ff) (node' l)    := []
 
 attribute [inverse]
 lemma unpack_pack {A : Sort*} : ∀ (l : list (tree A)), unpack (pack l) = l
diff --git a/tests/lean/run/soundness.lean b/tests/lean/run/soundness.lean
index 3b82199b94..55608e3a02 100644
--- a/tests/lean/run/soundness.lean
+++ b/tests/lean/run/soundness.lean
@@ -85,16 +85,16 @@ namespace PropF
   open Nc
 
   lemma weakening2 : ∀ {Γ A Δ}, Γ ⊢ A → Γ ⊆ Δ → Δ ⊢ A
-  | .Γ .A       Δ (Nax Γ A Hin)          Hs := Nax _ _ (Hs Hin)
-  | .Γ .(A ⇒ B) Δ (ImpI Γ A B H)         Hs := ImpI _ _ _ (weakening2 H (cons_subset_cons A Hs))
-  | .Γ .B       Δ (ImpE Γ A B H₁ H₂)     Hs := ImpE _ _ _ (weakening2 H₁ Hs) (weakening2 H₂ Hs)
-  | .Γ .A       Δ (BotC Γ A H)           Hs := BotC _ _ (weakening2 H (cons_subset_cons (~A) Hs))
-  | .Γ .(A ∧ B) Δ (AndI Γ A B H₁ H₂)     Hs := AndI _ _ _ (weakening2 H₁ Hs) (weakening2 H₂ Hs)
-  | .Γ .A       Δ (AndE₁ Γ A B H)        Hs := AndE₁ _ _ _ (weakening2 H Hs)
-  | .Γ .B       Δ (AndE₂ Γ A B H)        Hs := AndE₂ _ _ _ (weakening2 H Hs)
-  | .Γ .(A ∨ B) Δ (OrI₁ Γ A B H)         Hs := OrI₁ _ _ _ (weakening2 H Hs)
-  | .Γ .(A ∨ B) Δ (OrI₂ Γ A B H)         Hs := OrI₂ _ _ _ (weakening2 H Hs)
-  | .Γ .C       Δ (OrE Γ A B C H₁ H₂ H₃) Hs :=
+  | ._ ._       Δ (Nax Γ A Hin)          Hs := Nax _ _ (Hs Hin)
+  | ._ .(A ⇒ B) Δ (ImpI Γ A B H)         Hs := ImpI _ _ _ (weakening2 H (cons_subset_cons A Hs))
+  | ._ ._       Δ (ImpE Γ A B H₁ H₂)     Hs := ImpE _ _ _ (weakening2 H₁ Hs) (weakening2 H₂ Hs)
+  | ._ ._       Δ (BotC Γ A H)           Hs := BotC _ _ (weakening2 H (cons_subset_cons (~A) Hs))
+  | ._ .(A ∧ B) Δ (AndI Γ A B H₁ H₂)     Hs := AndI _ _ _ (weakening2 H₁ Hs) (weakening2 H₂ Hs)
+  | ._ ._       Δ (AndE₁ Γ A B H)        Hs := AndE₁ _ _ _ (weakening2 H Hs)
+  | ._ ._       Δ (AndE₂ Γ A B H)        Hs := AndE₂ _ _ _ (weakening2 H Hs)
+  | ._ .(A ∨ B) Δ (OrI₁ Γ A B H)         Hs := OrI₁ _ _ _ (weakening2 H Hs)
+  | ._ .(A ∨ B) Δ (OrI₂ Γ A B H)         Hs := OrI₂ _ _ _ (weakening2 H Hs)
+  | ._ ._       Δ (OrE Γ A B C H₁ H₂ H₃) Hs :=
        OrE _ _ _ _ (weakening2 H₁ Hs) (weakening2 H₂ (cons_subset_cons A Hs)) (weakening2 H₃ (cons_subset_cons B Hs))
 
   lemma weakening : ∀ Γ Δ A, Γ ⊢ A → Γ++Δ ⊢ A :=
@@ -117,8 +117,8 @@ namespace PropF
   attribute [simp] is_true TrueQ
 
   theorem Soundness_general {v : valuation} : ∀ {A Γ}, Γ ⊢ A → Satisfies v Γ → is_true (TrueQ v A)
-  | .A       .Γ (Nax Γ A Hin)  s  := s _ Hin
-  | .(A ⇒ B) .Γ (ImpI Γ A B H) s  :=
+  | ._      ._ (Nax Γ A Hin)  s  := s _ Hin
+  | .(A ⇒ B) ._ (ImpI Γ A B H) s  :=
     by_cases
       (λ t : is_true (TrueQ v A),
         have Satisfies v (A::Γ), from Satisfies_cons s t,
@@ -128,34 +128,34 @@ namespace PropF
         have TrueQ v A = ff, by simp at f; simph,
         have bnot (TrueQ v A) = tt, by simph,
         by simph)
-  | .B .Γ (ImpE Γ A B H₁ H₂) s :=
+  | ._ ._ (ImpE Γ A B H₁ H₂) s :=
     have aux : TrueQ v A = tt, from Soundness_general H₂ s,
     have bnot (TrueQ v A) || TrueQ v B = tt, from Soundness_general H₁ s,
     by simp [aux] at this; simph
-  | .A .Γ (BotC Γ A H) s := by_contradiction
+  | ._ ._ (BotC Γ A H) s := by_contradiction
     (λ n : TrueQ v A ≠ tt,
       have TrueQ v A    = ff, by {simp at n; simph},
       have TrueQ v (~A) = tt, begin change (bnot (TrueQ v A) || ff = tt), simph end,
       have Satisfies v ((~A)::Γ), from Satisfies_cons s this,
       have TrueQ v ⊥ = tt, from Soundness_general H this,
       absurd this ff_ne_tt)
-  | .(A ∧ B) .Γ (AndI Γ A B H₁ H₂) s :=
+  | .(A ∧ B) ._ (AndI Γ A B H₁ H₂) s :=
     have TrueQ v A = tt, from Soundness_general H₁ s,
     have TrueQ v B = tt, from Soundness_general H₂ s,
     by simph
-  | .A     .Γ (AndE₁ Γ A B H) s :=
+  | ._     ._ (AndE₁ Γ A B H) s :=
     have TrueQ v (A ∧ B) = tt, from Soundness_general H s,
     by simp [TrueQ] at this; simph [is_true]
-  | .B     .Γ (AndE₂ Γ A B H) s :=
+  | ._     ._ (AndE₂ Γ A B H) s :=
     have TrueQ v (A ∧ B) = tt, from Soundness_general H s,
     by simp at this; simph
-  | .(A ∨ B) .Γ (OrI₁ Γ A B H) s :=
+  | .(A ∨ B) ._ (OrI₁ Γ A B H) s :=
     have TrueQ v A = tt, from Soundness_general H s,
     by simph
-  | .(A ∨ B) .Γ (OrI₂ Γ A B H) s :=
+  | .(A ∨ B) ._ (OrI₂ Γ A B H) s :=
     have TrueQ v B = tt, from Soundness_general H s,
     by simph
-  | .C     .Γ (OrE Γ A B C H₁ H₂ H₃) s :=
+  | ._     ._ (OrE Γ A B C H₁ H₂ H₃) s :=
     have TrueQ v A || TrueQ v B = tt, from Soundness_general H₁ s,
     have or (TrueQ v A = tt) (TrueQ v B = tt), by simp at this; simph,
     or.elim this
diff --git a/tests/lean/run/unreachable_cases.lean b/tests/lean/run/unreachable_cases.lean
index 66d49b9245..ee09c3f88b 100644
--- a/tests/lean/run/unreachable_cases.lean
+++ b/tests/lean/run/unreachable_cases.lean
@@ -7,13 +7,13 @@ inductive ifin : ℕ → Type -- inductively defined fin-type
 open ifin
 
 definition foo {N : Type} : Π{n : ℕ}, N → ifin n → (N × ifin n)
-| (succ k) n (fz .k) := sorry
+| (succ k) n (fz .(k)) := sorry
 | (succ k) n (fs x) := sorry
 
 definition bar {N : Type} : Π{n : ℕ}, (N × ifin n) → (N × ifin n)
-| (succ k) (n, fz .k) := sorry
+| (succ k) (n, fz .(k)) := sorry
 | (succ k) (n, fs x) := sorry
 
 definition bar2 {N : Type} : Π{n : ℕ}, (N × ifin n) → (N × ifin n)
-| (succ k) (n, fz .k) := sorry
+| (succ k) (n, fz .(k)) := sorry
 | (succ k) (n, fs x) := sorry