diff --git a/src/library/blast/hypothesis.h b/src/library/blast/hypothesis.h
index 151b34500..79197b58f 100644
--- a/src/library/blast/hypothesis.h
+++ b/src/library/blast/hypothesis.h
@@ -23,18 +23,18 @@ using hypothesis_idx_map = typename lean::rb_map<unsigned, T, unsigned_cmp>;
 
 class hypothesis {
     friend class state;
-    name               m_name;     // for pretty printing
+    name               m_name;      // for pretty printing
     unsigned           m_active:1;
-    unsigned           m_depth;
-    hypothesis_idx_set m_deps;     // hypotheses used by the type and/or value of this hypothesis.
+    unsigned           m_dep_depth; // dependency depth
+    hypothesis_idx_set m_deps;      // hypotheses used by the type and/or value of this hypothesis.
     expr               m_type;
-    expr               m_value;    // justification for this object.
+    expr               m_value;     // justification for this object.
     // Remark: if blast::is_local(m_value) is true, then the hypothesis is an assumption
 public:
-    hypothesis():m_active(false), m_depth(0) {}
+    hypothesis():m_active(false), m_dep_depth(0) {}
     name const & get_name() const { return m_name; }
     bool is_active() const { return m_active; }
-    unsigned get_depth() const { return m_depth; }
+    unsigned get_dep_depth() const { return m_dep_depth; }
     hypothesis_idx_set const & get_backward_deps() const { return m_deps; }
     expr const & get_type() const { return m_type; }
     expr const & get_value() const { return m_value; }
diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp
index 7afbedc9f..783fe98d8 100644
--- a/src/library/blast/state.cpp
+++ b/src/library/blast/state.cpp
@@ -355,13 +355,16 @@ bool state::check_invariant() const {
 }
 #endif
 
-struct hypothesis_depth_lt {
+struct hypothesis_dep_depth_lt {
     state const & m_state;
-    hypothesis_depth_lt(state const & s): m_state(s) {}
+
+    hypothesis_dep_depth_lt(state const & s): m_state(s) {}
     bool operator()(unsigned hidx1, unsigned hidx2) const {
         hypothesis const * h1 = m_state.get(hidx1);
         hypothesis const * h2 = m_state.get(hidx2);
-        return h1 && h2 && h1->get_depth() < h2->get_depth() && (h1->get_depth() == h2->get_depth() && hidx1 < hidx2);
+        return
+            h1 && h2 && h1->get_dep_depth() < h2->get_dep_depth() &&
+            (h1->get_dep_depth() == h2->get_dep_depth() && hidx1 < hidx2);
     }
 };
 
@@ -369,7 +372,7 @@ void state::get_sorted_hypotheses(hypothesis_idx_buffer & r) const {
     m_context.for_each([&](unsigned hidx, hypothesis const &) {
             r.push_back(hidx);
         });
-    std::sort(r.begin(), r.end(), hypothesis_depth_lt(*this));
+    std::sort(r.begin(), r.end(), hypothesis_dep_depth_lt(*this));
 }
 
 void state::add_forward_dep(unsigned hidx_user, unsigned hidx_provider) {
@@ -396,8 +399,8 @@ void state::add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user) {
                 unsigned hidx_provider = href_index(l);
                 hypothesis const * h_provider = get(hidx_provider);
                 lean_assert(h_provider);
-                if (h_user.m_depth <= h_provider->m_depth)
-                    h_user.m_depth = h_provider->m_depth + 1;
+                if (h_user.m_dep_depth <= h_provider->m_dep_depth)
+                    h_user.m_dep_depth = h_provider->m_dep_depth + 1;
                 if (!h_user.m_deps.contains(hidx_provider)) {
                     h_user.m_deps.insert(hidx_provider);
                     add_forward_dep(hidx_user, hidx_provider);