From 8e9ccf8b6fb0ff7ed20cb64a5ded728aedde1d15 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 5 Mar 2015 14:28:10 -0800
Subject: [PATCH] chore(frontends/lean): remove 'dead' tokens

---
 src/frontends/lean/token_table.cpp | 2 +-
 src/frontends/lean/tokens.cpp      | 8 --------
 src/frontends/lean/tokens.h        | 2 --
 3 files changed, 1 insertion(+), 11 deletions(-)

diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 854446b28..26d7c01cc 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -90,7 +90,7 @@ void init_token_table(token_table & t) {
         {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "example", "coercion",
          "abbreviation",
          "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
-         "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]",
+         "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]",
          "[parsing-only]", "[multiple-instances]",
          "evaluate", "check", "eval", "[wf]", "[whnf]", "[all-transparent]", "[priority", "[unfold-c", "print",
          "end", "namespace", "section", "prelude",
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index e15e58a10..e360b8550 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -68,8 +68,6 @@ static name * g_exposing     = nullptr;
 static name * g_renaming     = nullptr;
 static name * g_extends      = nullptr;
 static name * g_as           = nullptr;
-static name * g_on           = nullptr;
-static name * g_off          = nullptr;
 static name * g_none         = nullptr;
 static name * g_whnf         = nullptr;
 static name * g_wf           = nullptr;
@@ -190,8 +188,6 @@ void initialize_tokens() {
     g_renaming     = new name("renaming");
     g_extends      = new name("extends");
     g_as           = new name("as");
-    g_on           = new name("[on]");
-    g_off          = new name("[off]");
     g_none         = new name("[none]");
     g_whnf         = new name("[whnf]");
     g_wf           = new name("[wf]");
@@ -320,8 +316,6 @@ void finalize_tokens() {
     delete g_renaming;
     delete g_extends;
     delete g_as;
-    delete g_on;
-    delete g_off;
     delete g_none;
     delete g_whnf;
     delete g_wf;
@@ -436,8 +430,6 @@ name const & get_exposing_tk() { return *g_exposing; }
 name const & get_renaming_tk() { return *g_renaming; }
 name const & get_extends_tk() { return *g_extends; }
 name const & get_as_tk() { return *g_as; }
-name const & get_on_tk() { return *g_on; }
-name const & get_off_tk() { return *g_off; }
 name const & get_none_tk() { return *g_none; }
 name const & get_whnf_tk() { return *g_whnf; }
 name const & get_wf_tk() { return *g_wf; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index 02a2c1876..3005615d8 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -70,8 +70,6 @@ name const & get_exposing_tk();
 name const & get_renaming_tk();
 name const & get_extends_tk();
 name const & get_as_tk();
-name const & get_on_tk();
-name const & get_off_tk();
 name const & get_none_tk();
 name const & get_whnf_tk();
 name const & get_wf_tk();