diff --git a/library/init/logic.lean b/library/init/logic.lean
index f0818079be..427529de70 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -223,16 +223,16 @@ theorem eq_rec_heq {A : Type} {P : A → Type} {a a' : A} (H : a = a') (p : P a)
 eq.drec_on H (heq.refl p)
 
 theorem heq_of_eq_rec_left {A : Type} {P : A → Type} : ∀ {a a' : A} {p₁ : P a} {p₂ : P a'} (e : a = a') (h₂ : eq.rec_on e p₁ = p₂), p₁ == p₂
-| a a p₁ p₂ (eq.refl a) h := eq.rec_on h (heq.refl p₁)
+| a ⌞a⌟ p₁ p₂ (eq.refl ⌞a⌟) h := eq.rec_on h (heq.refl p₁)
 
 theorem heq_of_eq_rec_right {A : Type} {P : A → Type} : ∀ {a a' : A} {p₁ : P a} {p₂ : P a'} (e : a' = a) (h₂ : p₁ = eq.rec_on e p₂), p₁ == p₂
-| a a p₁ p₂ (eq.refl a) h := eq.rec_on h (heq.refl p₁)
+| a ⌞a⌟ p₁ p₂ (eq.refl ⌞a⌟) h := eq.rec_on h (heq.refl p₁)
 
 theorem of_heq_true {a : Prop} (H : a == true) : a :=
 of_eq_true (eq_of_heq H)
 
 theorem eq_rec_compose : ∀ {A B C : Type} (p₁ : B = C) (p₂ : A = B) (a : A), eq.rec_on p₁ (eq.rec_on p₂ a : B) = eq.rec_on (eq.trans p₂ p₁) a
-| A A A (eq.refl A) (eq.refl A) a := calc
+| A ⌞A⌟ ⌞A⌟ (eq.refl ⌞A⌟) (eq.refl ⌞A⌟) a := calc
   eq.rec_on (eq.refl A) (eq.rec_on (eq.refl A) a) = eq.rec_on (eq.refl A) a               : rfl
             ...             = eq.rec_on (eq.trans (eq.refl A) (eq.refl A)) a  : eq.subst (proof_irrel (eq.refl A) (eq.trans (eq.refl A) (eq.refl A))) rfl
 
@@ -240,7 +240,7 @@ theorem eq_rec_eq_eq_rec {A₁ A₂ : Type} {p : A₁ = A₂} : ∀ {a₁ : A₁
 eq.drec_on p (λ a₁ a₂ h, eq.drec_on h rfl)
 
 theorem eq_rec_of_heq_left : ∀ {A₁ A₂ : Type} {a₁ : A₁} {a₂ : A₂} (h : a₁ == a₂), eq.rec_on (type_eq_of_heq h) a₁ = a₂
-| A A a a (heq.refl a) := rfl
+| A ⌞A⌟ a ⌞a⌟ (heq.refl ⌞a⌟) := rfl
 
 theorem eq_rec_of_heq_right {A₁ A₂ : Type} {a₁ : A₁} {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)
@@ -252,7 +252,7 @@ attribute heq_of_eq_of_heq [trans]
 attribute heq.symm [symm]
 
 theorem cast_heq : ∀ {A B : Type} (H : A = B) (a : A), cast H a == a
-| A A (eq.refl A) a := heq.refl a
+| A ⌞A⌟ (eq.refl ⌞A⌟) a := heq.refl a
 
 /- and -/
 
diff --git a/library/init/sigma.lean b/library/init/sigma.lean
index 704a36e65b..d56a30b172 100644
--- a/library/init/sigma.lean
+++ b/library/init/sigma.lean
@@ -29,7 +29,7 @@ namespace sigma
   variable  (Rb  : ∀ a, B a → B a → Prop)
 
   theorem dpair_eq : ∀ {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (H₁ : a₁ = a₂), eq.rec_on H₁ b₁ = b₂ → (sigma.mk a₁ b₁) = (sigma.mk a₂ b₂)
-  | a₁ a₁ b₁ b₁ (eq.refl a₁) (eq.refl b₁) := rfl
+  | a₁ ⌞a₁⌟ b₁ ⌞b₁⌟ (eq.refl ⌞a₁⌟) (eq.refl ⌞b₁⌟) := rfl
 
   protected theorem eq {p₁ p₂ : Σa : A, B a} :
     ∀(H₁ : p₁.1 = p₂.1) (H₂ : eq.rec_on H₁ p₁.2 = p₂.2), p₁ = p₂ :=
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index fcff3e2738..e1bd332836 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1611,16 +1611,51 @@ expr parser::parse_led_notation(expr left) {
     }
 }
 
+/**
+   \brief Auxiliary object for converting pattern_or_expr into a pattern.
+   The main points are:
+
+   1- Collect all pattern variables. Each pattern variable can only be
+      "declared" once. That is, the following equation is not valid
+
+        definition f : nat -> nat -> nat
+        | a a := a
+
+   2- We do not collect pattern variables inside inaccessible term (e.g., ⌞f a⌟)
+
+      Remark: An inaccessible term may contain a reference to a variable defined
+      later. Here is an example:
+
+      inductive imf {A B : Type} (f : A → B) : B → Type
+      | mk : ∀ (a : A), imf (f a)
+
+      definition inv {A B : Type} (f : A → B) : ∀ (b : B), imf f b → A
+      | ⌞f a⌟ (imf.mk ⌞f⌟ a)  := a
+
+      The 'a' in ⌞f a⌟ is a reference to the variable 'a' being declared at
+      (imf.mk ⌞f⌟ a)
+
+   3- The type in type ascriptions is implicitly marked as inaccessible.
+
+   4- An inaccessible term cannot be the function in an application.
+      Example: (⌞f⌟ a) is not allowed.
+
+   5- In a pattern (f a), f must be a constructor or a constant tagged with the
+      [pattern] attribute
+
+   6- A '_' is treated as an anonymous variable in patterns, and as placeholder
+      inside of inaccessible terms. */
 struct to_pattern_fn {
     parser &       m_parser;
     buffer<expr> & m_new_locals;
-    name_map<expr> m_vars;
-
-    environment const & env() { return m_parser.env(); }
+    name_map<expr> m_locals_map; // local variable name --> its interpretation
+    expr_map<expr> m_anonymous_vars; // for _
 
     to_pattern_fn(parser & p, buffer<expr> & new_locals):
         m_parser(p), m_new_locals(new_locals) {}
 
+    environment const & env() { return m_parser.env(); }
+
     /* Return true iff the constant n may occur in a pattern */
     bool is_pattern_constant(name const & n) {
         if (inductive::is_intro_rule(env(), n))
@@ -1630,13 +1665,13 @@ struct to_pattern_fn {
         return false;
     }
 
-    expr visit_local(expr const & e) {
-        if (auto r = m_vars.find(local_pp_name(e)))
-            return *r;
+    void collect_new_local(expr const & e) {
+        name const & n = local_pp_name(e);
         bool resolve_only = true;
-        expr new_e = m_parser.id_to_expr(local_pp_name(e), m_parser.pos_of(e), resolve_only);
+        expr new_e = m_parser.id_to_expr(n, m_parser.pos_of(e), resolve_only);
         if (is_constant(new_e) && is_pattern_constant(const_name(new_e))) {
-            return new_e;
+            m_locals_map.insert(n, new_e);
+            return;
         } else if (is_choice(new_e)) {
             bool all_pattern_constant = true;
             bool has_pattern_constant = false;
@@ -1648,7 +1683,8 @@ struct to_pattern_fn {
                     all_pattern_constant = false;
             }
             if (all_pattern_constant) {
-                return new_e;
+                m_locals_map.insert(n, new_e);
+                return;
             } else if (has_pattern_constant) {
                 throw parser_error(sstream() << "invalid pattern, '" << e << "' is overloaded, "
                                    << "and some interpretations may occur in patterns and others not "
@@ -1658,19 +1694,53 @@ struct to_pattern_fn {
                 // assume e is a variable shadowing overloaded constants
             }
         }
-        if (!local_pp_name(e).is_atomic()) {
+        if (!n.is_atomic()) {
             throw parser_error("invalid pattern, variable, constructor or constant tagged as pattern expected",
                                m_parser.pos_of(e));
         }
-        m_vars.insert(local_pp_name(e), e);
+        if (m_locals_map.contains(n)) {
+            throw parser_error(sstream() << "invalid pattern, '" << n << "' already appeared in this pattern",
+                               m_parser.pos_of(e));
+        }
+        m_locals_map.insert(n, e);
         m_new_locals.push_back(e);
-        return e;
+    }
+
+    void collect_new_locals(expr const & e, bool skip_main_fn) {
+        if (is_typed_expr(e)) {
+            collect_new_locals(get_typed_expr_expr(e), false);
+        } else if (is_prenum(e)) {
+            // do nothing
+        } else if (is_inaccessible(e)) {
+            // do nothing
+        } else if (is_placeholder(e)) {
+            expr r = mk_local(mk_fresh_name(), "_x", mk_expr_placeholder(), binder_info());
+            m_new_locals.push_back(r);
+            m_anonymous_vars.insert(mk_pair(e, r));
+        } else if (is_app(e)) {
+            collect_new_locals(app_fn(e), skip_main_fn);
+            collect_new_locals(app_arg(e), false);
+        } else if (is_local(e)) {
+            if (skip_main_fn) {
+                // do nothing
+            } else {
+                collect_new_local(e);
+            }
+        } else if (is_annotation(e)) {
+            collect_new_locals(get_annotation_arg(e), skip_main_fn);
+        } else if (is_constant(e) && is_pattern_constant(const_name(e))) {
+            // do nothing
+        } else {
+            throw parser_error("invalid pattern, must be an application, "
+                               "constant, variable, type ascription or inaccessible term",
+                               m_parser.pos_of(e));
+        }
     }
 
     expr to_expr(expr const & e) {
         return replace(e, [&](expr const & e, unsigned) {
                 if (is_local(e)) {
-                    if (auto r = m_vars.find(local_pp_name(e)))
+                    if (auto r = m_locals_map.find(local_pp_name(e)))
                         return some_expr(*r);
                     else
                         return some_expr(m_parser.patexpr_to_expr(e));
@@ -1679,9 +1749,9 @@ struct to_pattern_fn {
             });
     }
 
-    expr visit(expr const & e, bool skip_main_fn) {
+    expr visit(expr const & e) {
         if (is_typed_expr(e)) {
-            expr new_v = visit(get_typed_expr_expr(e), false);
+            expr new_v = visit(get_typed_expr_expr(e));
             expr new_t = to_expr(get_typed_expr_type(e));
             return copy_tag(e, mk_typed_expr(new_t, new_v));
         } else if (is_prenum(e)) {
@@ -1689,20 +1759,22 @@ struct to_pattern_fn {
         } else if (is_inaccessible(e)) {
             return to_expr(e);
         } else if (is_placeholder(e)) {
-            expr r = mk_local(mk_fresh_name(), "_x", mk_expr_placeholder(), binder_info());
-            m_new_locals.push_back(r);
-            return r;
+            return m_anonymous_vars.find(e)->second;
         } else if (is_app(e)) {
-            expr new_f = visit(app_fn(e), skip_main_fn);
-            expr new_a = visit(app_arg(e), false);
+            if (is_inaccessible(app_fn(e))) {
+                throw parser_error("invalid inaccessible annotation, it cannot be used around functions in applications",
+                                   m_parser.pos_of(e));
+            }
+            expr new_f = visit(app_fn(e));
+            expr new_a = visit(app_arg(e));
             return update_app(e, new_f, new_a);
         } else if (is_local(e)) {
-            if (skip_main_fn)
-                return e;
+            if (auto r = m_locals_map.find(local_pp_name(e)))
+                return *r;
             else
-                return visit_local(e);
+                return e;
         } else if (is_annotation(e)) {
-            return copy_tag(e, mk_annotation(get_annotation_kind(e), visit(get_annotation_arg(e), skip_main_fn)));
+            return copy_tag(e, mk_annotation(get_annotation_kind(e), visit(get_annotation_arg(e))));
         } else if (is_constant(e) && is_pattern_constant(const_name(e))) {
             return e;
         } else {
@@ -1713,7 +1785,9 @@ struct to_pattern_fn {
     }
 
     expr operator()(expr const & e, bool skip_main_fn) {
-        return visit(e, skip_main_fn);
+        collect_new_locals(e, skip_main_fn);
+        expr r = visit(e);
+        return r;
     }
 };
 
diff --git a/tests/lean/inaccessible.lean b/tests/lean/inaccessible.lean
new file mode 100644
index 0000000000..2a88e96743
--- /dev/null
+++ b/tests/lean/inaccessible.lean
@@ -0,0 +1,82 @@
+inductive imf {A B : Type} (f : A → B) : B → Type
+| mk : ∀ (a : A), imf (f a)
+
+definition inv_1 {A B : Type} (f : A → B) : ∀ (b : B), imf f b → A
+| ⌞f a⌟ (imf.mk ⌞f⌟ a)  := a
+
+definition inv_2 {A B : Type} (f : A → B) : ∀ (b : B), imf f b → A
+| ⌞_⌟ (imf.mk ⌞_⌟ a)  := a
+
+definition mk {A B : Type} {f : A → B} (a : A) := imf.mk f a
+
+definition inv_3 {A B : Type} (f : A → B) : ∀ (b : B), imf f b → A
+| ⌞f a⌟ (mk a)  := a -- Error, mk is not a constructor
+
+definition inv_4 {A B : Type} (f : A → B) : ∀ (b : B), imf f b → A
+| ⌞f a⌟ (⌞mk⌟ a)  := a -- Error, we cannot use inaccessible annotation around functions in applications
+
+attribute [pattern] mk
+
+definition inv_5 {A B : Type} (f : A → B) : ∀ (b : B), imf f b → A
+| ⌞f a⌟ (mk a)  := a
+
+definition inv_6 {A B : Type} (f : A → B) : ∀ (b : B), imf f b → A
+| (f a) (mk a)  := a  -- Error, 'a' is being "declared" twice in the pattern
+
+definition inv_7 {A B : Type} (f : A → B) : ∀ (b : B), imf f b → A
+| (f a) (mk b)  := a  -- Typing error, it would also fail when compiling the pattern
+
+definition g_1 : nat → nat → nat
+| a a := a   -- Error, 'a' is being "declared" twice
+
+definition g_2 (a : nat) : nat → nat → nat
+| a b := a
+
+example (a b c : nat) : g_2 a b c = b :=
+rfl
+
+inductive vec1 (A : Type) : nat → Type
+| nil  : vec1 0
+| cons : ∀ n, A → vec1 n → vec1 (n+1)
+
+section
+open vec1
+
+definition map_1 {A : Type} (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₂)
+
+definition map_2 {A : Type} (f : A → A → A) : Π {n}, vec1 A n → vec1 A n → vec1 A n
+| 0     (nil ⌞_⌟)        (nil ⌞_⌟)        := nil A
+| (n+1) (cons ⌞_⌟ h₁ v₁) (cons ⌞_⌟ h₂ v₂) := cons n (f h₁ h₂) (map_2 v₁ v₂)
+
+/- In map_3, we use the inaccessible terms to avoid pattern/matching on the first argument -/
+definition map_3 {A : Type} (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₂)
+end
+
+inductive vec2 (A : Type) : nat → Type
+| nil {} : vec2 0
+| cons   : ∀ {n}, A → vec2 n → vec2 (n+1)
+
+section
+open vec2
+
+definition map_4 {A : Type} (f : A → A → A) : Π {n}, vec2 A n → vec2 A n → vec2 A n
+| 0     nil          nil          := nil
+| (n+1) (cons h₁ v₁) (cons h₂ v₂) := cons (f h₁ h₂) (map_4 v₁ v₂)
+
+definition map_5 {A : Type} (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₂)
+
+/-
+The following variant will be rejected by the new equation compiler.
+In Lean2, the second equation is accepted because unassigned metavariables
+occurring in patterns become new variables. This feature is too hackish.
+-/
+definition map_6 {A : Type} (f : A → A → A) : Π {n}, vec2 A n → vec2 A n → vec2 A n
+| ⌞_⌟  nil          nil         := nil
+| ⌞_⌟ (cons h₁ v₁) (cons h₂ v₂) := cons (f h₁ h₂) (map_6 v₁ v₂)
+end
diff --git a/tests/lean/inaccessible.lean.expected.out b/tests/lean/inaccessible.lean.expected.out
new file mode 100644
index 0000000000..ec6032dc18
--- /dev/null
+++ b/tests/lean/inaccessible.lean.expected.out
@@ -0,0 +1,17 @@
+inaccessible.lean:13:9: error: invalid argument, it is not a constructor, variable, nor it is marked as an inaccessible pattern
+  mk a
+in the following equation left-hand-side
+  inv_3 ⌞f a⌟ (mk a)
+inaccessible.lean:16:10: error: invalid inaccessible annotation, it cannot be used around functions in applications
+inaccessible.lean:24:12: error: invalid pattern, 'a' already appeared in this pattern
+inaccessible.lean:27:9: error: type mismatch at application
+  inv_7 (f_1 a) (mk b)
+term
+  mk b
+has type
+  imf f (f b)
+but is expected to have type
+  imf f (f_1 a)
+The following identifier(s) are introduced as free variables by the left-hand-side of the equation:
+  f a b 
+inaccessible.lean:30:4: error: invalid pattern, 'a' already appeared in this pattern
diff --git a/tests/lean/run/eq2.lean b/tests/lean/run/eq2.lean
index 6ebf0d1cde..fbdfc36f76 100644
--- a/tests/lean/run/eq2.lean
+++ b/tests/lean/run/eq2.lean
@@ -1,5 +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