diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp
index 544ec229f..2fd36512f 100644
--- a/src/frontends/lean/notation_cmd.cpp
+++ b/src/frontends/lean/notation_cmd.cpp
@@ -136,13 +136,13 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, nota
             if (auto ls = get_reserved_nud_table(p.env()).find(tks)) {
                 // Remark: we are ignoring multiple actions in the reserved notation table
                 reserved_pt     = head(ls).second;
-                reserved_action = head(ls).first;
+                reserved_action = head(ls).first.get_action();
             }
         } else {
             if (auto ls = get_reserved_led_table(p.env()).find(tks)) {
                 // Remark: we are ignoring multiple actions in the reserved notation table
                 reserved_pt     = head(ls).second;
-                reserved_action = head(ls).first;
+                reserved_action = head(ls).first.get_action();
             }
         }
     }
@@ -413,8 +413,8 @@ static unsigned get_default_prec(optional<parse_table> const & pt, name const &
         return LEAN_DEFAULT_PRECEDENCE;
     if (auto ls = pt->find(tk)) {
         for (auto at : ls) {
-            if (at.first.kind() == notation::action_kind::Expr)
-                return at.first.rbp();
+            if (at.first.get_action().kind() == notation::action_kind::Expr)
+                return at.first.get_action().rbp();
         }
     }
     return LEAN_DEFAULT_PRECEDENCE;
@@ -426,7 +426,7 @@ static optional<parse_table> find_match(optional<parse_table> const & pt, transi
     if (pt) {
         if (auto ls = pt->find(new_trans.get_token())) {
             for (auto at : ls) {
-                if (new_trans.get_action().is_equal(at.first))
+                if (new_trans.get_action().is_equal(at.first.get_action()))
                     return optional<parse_table>(at.second);
             }
         }
@@ -435,11 +435,11 @@ static optional<parse_table> find_match(optional<parse_table> const & pt, transi
 }
 
 /** \brief Lift parse_table::find method to optional<parse_table> */
-static list<pair<action, parse_table>> find_next(optional<parse_table> const & pt, name const & tk) {
+static list<pair<transition, parse_table>> find_next(optional<parse_table> const & pt, name const & tk) {
     if (pt)
         return pt->find(tk);
     else
-        return list<pair<action, parse_table>>();
+        return list<pair<transition, parse_table>>();
 }
 
 static unsigned parse_binders_rbp(parser & p) {
@@ -514,7 +514,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, notation_en
         name tk = parse_quoted_symbol_or_token(p, new_tokens, used_default, grp);
         if (auto at = find_next(reserved_pt, tk)) {
             // Remark: we are ignoring multiple actions in the reserved notation table
-            action const & a = head(at).first;
+            action const & a = head(at).first.get_action();
             reserved_pt      = head(at).second;
             switch (a.kind()) {
             case notation::action_kind::Skip:
diff --git a/src/frontends/lean/parse_table.cpp b/src/frontends/lean/parse_table.cpp
index 1ba5fe954..e998ad815 100644
--- a/src/frontends/lean/parse_table.cpp
+++ b/src/frontends/lean/parse_table.cpp
@@ -331,9 +331,9 @@ transition replace(transition const & t, std::function<expr(expr const &)> const
 }
 
 struct parse_table::cell {
-    bool                                      m_nud;
-    list<accepting>                           m_accept;
-    name_map<list<pair<action, parse_table>>> m_children;
+    bool                                          m_nud;
+    list<accepting>                               m_accept;
+    name_map<list<pair<transition, parse_table>>> m_children;
     MK_LEAN_RC(); // Declare m_rc counter
     void dealloc() { delete this; }
     cell(bool nud = true):m_nud(nud), m_rc(1) {}
@@ -347,12 +347,12 @@ parse_table::parse_table(parse_table && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
 parse_table::~parse_table() { if (m_ptr) m_ptr->dec_ref(); }
 parse_table & parse_table::operator=(parse_table const & s) { LEAN_COPY_REF(s); }
 parse_table & parse_table::operator=(parse_table && s) { LEAN_MOVE_REF(s); }
-list<pair<action, parse_table>> parse_table::find(name const & tk) const {
-    list<pair<action, parse_table>> const * it = m_ptr->m_children.find(tk);
+list<pair<transition, parse_table>> parse_table::find(name const & tk) const {
+    list<pair<transition, parse_table>> const * it = m_ptr->m_children.find(tk);
     if (it)
         return *it;
     else
-        return list<pair<action, parse_table>>();
+        return list<pair<transition, parse_table>>();
 }
 
 list<accepting> const & parse_table::is_accepting() const {
@@ -397,9 +397,9 @@ static list<accepting> insert(list<accepting> const & l, unsigned priority, list
     }
 }
 
-static bool contains_equivalent_action(list<pair<action, parse_table>> const & l, action const & a) {
+static bool contains_equivalent_action(list<pair<transition, parse_table>> const & l, action const & a) {
     for (auto const & p : l) {
-        if (p.first.is_equivalent(a))
+        if (p.first.get_action().is_equivalent(a))
             return true;
     }
     return false;
@@ -419,18 +419,18 @@ parse_table parse_table::add_core(unsigned num, transition const * ts, expr cons
             r.m_ptr->m_accept = insert(new_accept, priority, postponed, a);
         }
     } else {
-        list<pair<action, parse_table>> const * it = r.m_ptr->m_children.find(ts->get_token());
+        list<pair<transition, parse_table>> const * it = r.m_ptr->m_children.find(ts->get_token());
         action const & ts_act = ts->get_action();
         action_kind k = ts_act.kind();
         if (k == action_kind::Exprs || k == action_kind::ScopedExpr)
             post_buffer.push_back(ts_act);
-        list<pair<action, parse_table>> new_lst;
+        list<pair<transition, parse_table>> new_lst;
         if (it) {
             if (contains_equivalent_action(*it, ts_act)) {
-                buffer<pair<action, parse_table>> tmp;
+                buffer<pair<transition, parse_table>> tmp;
                 to_buffer(*it, tmp);
-                for (pair<action, parse_table> & p : tmp) {
-                    if (p.first.is_equivalent(ts_act)) {
+                for (pair<transition, parse_table> & p : tmp) {
+                    if (p.first.get_action().is_equivalent(ts_act)) {
                         p.second = p.second.add_core(num-1, ts+1, a, priority, overload, post_buffer);
                         break;
                     }
@@ -438,15 +438,15 @@ parse_table parse_table::add_core(unsigned num, transition const * ts, expr cons
                 new_lst = to_list(tmp);
             } else {
                 // remove incompatible actions
-                new_lst = filter(*it, [&](pair<action, parse_table> const & p) {
-                        return p.first.is_compatible(ts_act);
+                new_lst = filter(*it, [&](pair<transition, parse_table> const & p) {
+                        return p.first.get_action().is_compatible(ts_act);
                     });
                 parse_table new_child = parse_table().add_core(num-1, ts+1, a, priority, overload, post_buffer);
-                new_lst   = cons(mk_pair(ts_act, new_child), new_lst);
+                new_lst   = cons(mk_pair(*ts, new_child), new_lst);
             }
         } else {
             parse_table new_child = parse_table().add_core(num-1, ts+1, a, priority, overload, post_buffer);
-            new_lst   = to_list(mk_pair(ts_act, new_child));
+            new_lst   = to_list(mk_pair(*ts, new_child));
         }
         r.m_ptr->m_children.insert(ts->get_token(), new_lst);
     }
@@ -527,9 +527,9 @@ void parse_table::for_each(buffer<transition> & ts,
                                               list<accepting> const &)> const & fn) const {
     if (!is_nil(m_ptr->m_accept))
         fn(ts.size(), ts.data(), m_ptr->m_accept);
-    m_ptr->m_children.for_each([&](name const & k, list<pair<action, parse_table>> const & lst) {
+    m_ptr->m_children.for_each([&](name const & k, list<pair<transition, parse_table>> const & lst) {
             for (auto const & p : lst) {
-                ts.push_back(transition(k, p.first));
+                ts.push_back(p.first);
                 p.second.for_each(ts, fn);
                 ts.pop_back();
             }
@@ -773,11 +773,11 @@ static int merge(lua_State * L) {
 }
 
 static int find(lua_State * L) {
-    list<pair<action, parse_table>> it = to_parse_table(L, 1).find(to_name_ext(L, 2));
+    list<pair<transition, parse_table>> it = to_parse_table(L, 1).find(to_name_ext(L, 2));
     if (it) {
         // TODO(Leo): support multiple actions
         auto p = head(it);
-        push_notation_action(L, p.first);
+        push_notation_action(L, p.first.get_action());
         push_parse_table(L, p.second);
         return 2;
     } else {
diff --git a/src/frontends/lean/parse_table.h b/src/frontends/lean/parse_table.h
index 91f94a9a5..236930122 100644
--- a/src/frontends/lean/parse_table.h
+++ b/src/frontends/lean/parse_table.h
@@ -173,7 +173,7 @@ public:
         return add(ts.size(), ts.begin(), a, LEAN_DEFAULT_NOTATION_PRIORITY, true);
     }
     parse_table merge(parse_table const & s, bool overload) const;\
-    list<pair<action, parse_table>> find(name const & tk) const;
+    list<pair<transition, parse_table>> find(name const & tk) const;
     list<accepting> const & is_accepting() const;
     void for_each(std::function<void(unsigned, transition const *, list<accepting> const &)> const & fn) const;
 
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index d88149492..63741541e 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1175,9 +1175,9 @@ void parser::process_postponed(buffer<expr> const & args, bool is_left,
 }
 
 // Return true iff the current token is the terminator of some Exprs action, and store the matching pair in r
-static bool curr_is_terminator_of_exprs_action(parser const & p, list<pair<notation::action, parse_table>> const & lst, pair<notation::action, parse_table> const * & r) {
+static bool curr_is_terminator_of_exprs_action(parser const & p, list<pair<notation::transition, parse_table>> const & lst, pair<notation::transition, parse_table> const * & r) {
     for (auto const & pr : lst) {
-        notation::action const & a = pr.first;
+        notation::action const & a = pr.first.get_action();
         if (a.kind() == notation::action_kind::Exprs &&
             a.get_terminator() &&
             p.curr_is_token(*a.get_terminator())) {
@@ -1189,9 +1189,9 @@ static bool curr_is_terminator_of_exprs_action(parser const & p, list<pair<notat
 }
 
 // Return true iff \c lst contains a Skip action, and store the matching pair in r.
-static bool has_skip(list<pair<notation::action, parse_table>> const & lst, pair<notation::action, parse_table> const * & r) {
+static bool has_skip(list<pair<notation::transition, parse_table>> const & lst, pair<notation::transition, parse_table> const * & r) {
     for (auto const & p : lst) {
-        notation::action const & a = p.first;
+        notation::action const & a = p.first.get_action();
         if (a.kind() == notation::action_kind::Skip) {
             r = &p;
             return true;
@@ -1200,9 +1200,9 @@ static bool has_skip(list<pair<notation::action, parse_table>> const & lst, pair
     return false;
 }
 
-static pair<notation::action, parse_table> const * get_non_skip(list<pair<notation::action, parse_table>> const & lst) {
+static pair<notation::transition, parse_table> const * get_non_skip(list<pair<notation::transition, parse_table>> const & lst) {
     for (auto const & p : lst) {
-        notation::action const & a = p.first;
+        notation::action const & a = p.first.get_action();
         if (a.kind() != notation::action_kind::Skip)
             return &p;
     }
@@ -1234,26 +1234,26 @@ expr parser::parse_notation_core(parse_table t, expr * left, bool as_tactic) {
         auto r = t.find(get_token_info().value());
         if (!r)
             break;
-        pair<notation::action, parse_table> const * curr_pair = nullptr;
+        pair<notation::transition, parse_table> const * curr_pair = nullptr;
         if (tail(r)) {
             // There is more than one possible actions.
             // In the current implementation, we support the following possible cases (Skip, Expr), (Skip, Exprs) amd (Skip, ScopedExpr)
             next();
             if (curr_is_terminator_of_exprs_action(*this, r, curr_pair)) {
-                lean_assert(curr_pair->first.kind() == notation::action_kind::Exprs);
+                lean_assert(curr_pair->first.get_action().kind() == notation::action_kind::Exprs);
             } else if (has_skip(r, curr_pair) && !curr_starts_expr()) {
-                lean_assert(curr_pair->first.kind() == notation::action_kind::Skip);
+                lean_assert(curr_pair->first.get_action().kind() == notation::action_kind::Skip);
             } else {
                 curr_pair = get_non_skip(r);
             }
         } else {
             // there is only one possible action
             curr_pair = &head(r);
-            if (curr_pair->first.kind() != notation::action_kind::Ext)
+            if (curr_pair->first.get_action().kind() != notation::action_kind::Ext)
                 next();
         }
         lean_assert(curr_pair);
-        notation::action const & a = curr_pair->first;
+        notation::action const & a = curr_pair->first.get_action();
         switch (a.kind()) {
         case notation::action_kind::Skip:
             break;