diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp
index d5b3a3a9c..654d53ee0 100644
--- a/src/library/blast/blast.cpp
+++ b/src/library/blast/blast.cpp
@@ -616,7 +616,7 @@ public:
         imp_extension * imp_ext = _imp_ext;
         while (imp_ext != nullptr) {
             path.push_back(imp_ext);
-            imp_ext = imp_ext->m_parent;
+            imp_ext = imp_ext->get_parent();
         }
     }
 
diff --git a/src/library/blast/imp_extension.cpp b/src/library/blast/imp_extension.cpp
index 36d512354..65bdc68eb 100644
--- a/src/library/blast/imp_extension.cpp
+++ b/src/library/blast/imp_extension.cpp
@@ -8,7 +8,6 @@ Author: Daniel Selsam
 
 namespace lean {
 namespace blast {
-
 imp_extension::imp_extension(unsigned state_id): m_state_id(state_id), m_parent(nullptr) {}
 imp_extension::imp_extension(imp_extension * parent):
     m_state_id(parent->m_state_id), m_parent(parent) {
@@ -40,5 +39,4 @@ void imp_extension_state::undo_actions(imp_extension * imp_ext) {
     if (is_nil(asserts)) return;
     pop();
 }
-
 }}
diff --git a/src/library/blast/imp_extension.h b/src/library/blast/imp_extension.h
index 71cd6b1ec..52ba04113 100644
--- a/src/library/blast/imp_extension.h
+++ b/src/library/blast/imp_extension.h
@@ -9,11 +9,11 @@ Author: Daniel Selsam
 namespace lean {
 namespace blast {
 
-struct imp_extension : branch_extension {
+class imp_extension : public branch_extension {
     unsigned              m_state_id;
     imp_extension *       m_parent;
     list<hypothesis>      m_asserts;
-
+public:
     imp_extension(unsigned state_id);
     imp_extension(imp_extension * parent);
     ~imp_extension();
@@ -26,7 +26,8 @@ struct imp_extension : branch_extension {
     virtual void hypothesis_activated(hypothesis const & h, hypothesis_idx hidx) override;
 };
 
-struct imp_extension_state {
+class imp_extension_state {
+public:
     virtual void push() =0;
     virtual void pop()  =0;
     virtual void assert(hypothesis const & h) =0;
@@ -38,5 +39,4 @@ struct imp_extension_state {
 };
 
 typedef std::function<imp_extension_state*()> ext_state_maker;
-
 }}