From 30d20e8029046f47b0a1133c7a68fe73ab8c307e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 11 Feb 2015 16:29:58 -0800
Subject: [PATCH] chore(frontends/lean/parser): remove dead code

---
 src/frontends/lean/parser.cpp | 13 -------------
 src/frontends/lean/parser.h   |  1 -
 2 files changed, 14 deletions(-)

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 4f17f6196..5fc97870c 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -354,19 +354,6 @@ expr parser::copy_with_new_pos(expr const & e, pos_info p) {
     lean_unreachable(); // LCOV_EXCL_LINE
 }
 
-/** \brief Add \c ls to constants occurring in \c e. */
-expr parser::propagate_levels(expr const & e, levels const & ls) {
-    if (is_nil(ls)) {
-        return e;
-    } else {
-        return replace(e, [&](expr const & e) {
-                if (is_constant(e))
-                    return some_expr(update_constant(e, ls));
-                return none_expr();
-            });
-    }
-}
-
 pos_info parser::pos_of(expr const & e, pos_info default_pos) const {
     tag t = e.get_tag();
     if (t == nulltag)
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index ecf5bfe03..9f9a4a187 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -164,7 +164,6 @@ class parser {
 
     tag get_tag(expr e);
     expr copy_with_new_pos(expr const & e, pos_info p);
-    expr propagate_levels(expr const & e, levels const & ls);
 
     cmd_table const & cmds() const { return get_cmd_table(env()); }
     parse_table const & nud() const { return get_nud_table(env()); }