diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 36ee3c1ca8a..512e367efa9 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -39,7 +39,6 @@ Module Name:
 #include "solver/progress_callback.h"
 #include "cmd_context/pdecl.h"
 #include "cmd_context/tactic_manager.h"
-#include "cmd_context/proof_cmds.h"
 #include "params/context_params.h"
 
 
@@ -94,8 +93,7 @@ class macro_decls {
 
 class proof_cmds {
 public:
-    proof_cmds(ast_manager& m);
-    virtual ~proof_cmds();
+    virtual ~proof_cmds() {}
     virtual void add_literal(expr* e) = 0;
     virtual void end_assumption() = 0;
     virtual void end_learned() = 0;
@@ -412,7 +410,7 @@ class cmd_context : public progress_callback, public tactic_manager, public ast_
     pdecl_manager & pm() const { if (!m_pmanager) const_cast<cmd_context*>(this)->init_manager(); return *m_pmanager; }
     sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast<cmd_context*>(this)->m_sexpr_manager = alloc(sexpr_manager); return *m_sexpr_manager; }
 
-    proof_cmds* get_proof_cmds() { return m_proof_cmds; }
+    proof_cmds* get_proof_cmds() { return m_proof_cmds.get(); }
     void set_proof_cmds(proof_cmds* pc) { m_proof_cmds = pc; }
 
     void set_solver_factory(solver_factory * s);
diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp
index 7c81d221197..d0d0b452dd0 100644
--- a/src/shell/smtlib_frontend.cpp
+++ b/src/shell/smtlib_frontend.cpp
@@ -26,7 +26,7 @@ Revision History:
 #include "parsers/smt2/smt2parser.h"
 #include "muz/fp/dl_cmds.h"
 #include "cmd_context/extra_cmds/dbg_cmds.h"
-#include "cmd_context/proof_cmds.h"
+#include "cmd_context/extra_cmds/proof_cmds.h"
 #include "opt/opt_cmds.h"
 #include "cmd_context/extra_cmds/polynomial_cmds.h"
 #include "cmd_context/extra_cmds/subpaving_cmds.h"