diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 39343ca86..c389c1429 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -511,13 +511,8 @@ cmd_table init_cmd_table() {
     add_cmd(r, cmd_info("abbreviation", "add new abbreviation (aka transparent definition)", abbreviation_cmd));
     add_cmd(r, cmd_info("theorem",      "add new theorem", theorem_cmd));
     add_cmd(r, cmd_info("check",        "type check given expression, and display its type", check_cmd));
-    add_cmd(r, cmd_info("precedence",   "set token left binding power", precedence_cmd));
-    add_cmd(r, cmd_info("infixl",       "declare a new infix (left) notation", infixl_cmd));
-    add_cmd(r, cmd_info("infix",        "declare a new infix (left) notation", infixl_cmd));
-    add_cmd(r, cmd_info("infixr",       "declare a new infix (right) notation", infixr_cmd));
-    add_cmd(r, cmd_info("postfix",      "declare a new postfix notation", postfix_cmd));
-    add_cmd(r, cmd_info("notation",     "declare a new notation", notation_cmd));
     add_cmd(r, cmd_info("#setline",     "modify the current line number, it only affects error/report messages", set_line_cmd));
+    register_notation_cmds(r);
     register_calc_cmds(r);
     return r;
 }
diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp
index 6c695225e..dfaa18bcc 100644
--- a/src/frontends/lean/notation_cmd.cpp
+++ b/src/frontends/lean/notation_cmd.cpp
@@ -297,4 +297,18 @@ notation_entry parse_notation(parser & p, bool overload, buffer<token_entry> & n
         throw parser_error("invalid notation, 'infix', 'infixl', 'infixr', 'postfix' or 'notation' expected", p.pos());
     }
 }
+
+environment notation_cmd(parser & p) { return notation_cmd_core(p, true); }
+environment infixl_cmd(parser & p) { return infixl_cmd_core(p, true); }
+environment infixr_cmd(parser & p) { return infixr_cmd_core(p, true); }
+environment postfix_cmd(parser & p) { return postfix_cmd_core(p, true); }
+
+void register_notation_cmds(cmd_table & r) {
+    add_cmd(r, cmd_info("precedence",   "set token left binding power", precedence_cmd));
+    add_cmd(r, cmd_info("infixl",       "declare a new infix (left) notation", infixl_cmd));
+    add_cmd(r, cmd_info("infix",        "declare a new infix (left) notation", infixl_cmd));
+    add_cmd(r, cmd_info("infixr",       "declare a new infix (right) notation", infixr_cmd));
+    add_cmd(r, cmd_info("postfix",      "declare a new postfix notation", postfix_cmd));
+    add_cmd(r, cmd_info("notation",     "declare a new notation", notation_cmd));
+}
 }
diff --git a/src/frontends/lean/notation_cmd.h b/src/frontends/lean/notation_cmd.h
index 7f004107d..e12d83c08 100644
--- a/src/frontends/lean/notation_cmd.h
+++ b/src/frontends/lean/notation_cmd.h
@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "kernel/environment.h"
 #include "frontends/lean/parser_config.h"
+#include "frontends/lean/cmd_table.h"
 namespace lean {
 class parser;
 
@@ -15,13 +16,11 @@ environment notation_cmd_core(parser & p, bool overload);
 environment infixl_cmd_core(parser & p, bool overload);
 environment infixr_cmd_core(parser & p, bool overload);
 environment postfix_cmd_core(parser & p, bool overload);
-inline environment notation_cmd(parser & p) { return notation_cmd_core(p, true); }
-inline environment infixl_cmd(parser & p) { return infixl_cmd_core(p, true); }
-inline environment infixr_cmd(parser & p) { return infixr_cmd_core(p, true); }
-inline environment postfix_cmd(parser & p) { return postfix_cmd_core(p, true); }
 
 /** \brief Return true iff the current token is a notation declaration */
 bool curr_is_notation_decl(parser & p);
 /** \brief Parse a notation declaration, throws an error if the current token is not a "notation declaration". */
 notation_entry parse_notation(parser & p, bool overload, buffer<token_entry> & new_tokens);
+
+void register_notation_cmds(cmd_table & r);
 }