diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp
index 36c961d65..21c7131e4 100644
--- a/src/library/tactic/proof_state.cpp
+++ b/src/library/tactic/proof_state.cpp
@@ -69,7 +69,7 @@ proof_state to_proof_state(expr const & mvar, name_generator ngen) {
     }
     expr meta = mk_app(mvar, ls);
     goals gs(goal(meta, t));
-    return proof_state(gs, substitution(), ngen, meta);
+    return proof_state(gs, substitution(), ngen);
 }
 
 static name g_tmp_prefix = name::mk_internal_unique_name();
@@ -163,7 +163,7 @@ static int mk_proof_state(lua_State * L) {
     } else if (nargs == 3) {
         return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2), to_substitution(L, 3)));
     } else if (nargs == 4) {
-        return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2), to_substitution(L, 3), to_name_generator(L, 4)));
+        return push_proof_state(L, proof_state(to_goals(L, 1), to_substitution(L, 2), to_name_generator(L, 3)));
     } else {
         throw exception("proof_state invalid number of arguments");
     }
@@ -191,7 +191,6 @@ static int proof_state_tostring(lua_State * L) {
 static int proof_state_get_goals(lua_State * L) { return push_goals(L, to_proof_state(L, 1).get_goals()); }
 static int proof_state_get_ngen(lua_State * L) { return push_name_generator(L, to_proof_state(L, 1).get_ngen()); }
 static int proof_state_get_subst(lua_State * L) { return push_substitution(L, to_proof_state(L, 1).get_subst()); }
-static int proof_state_get_initial(lua_State * L) { return push_list_expr(L, to_proof_state(L, 1).get_initial()); }
 static int proof_state_is_final_state(lua_State * L) { return push_boolean(L, to_proof_state(L, 1).is_final_state()); }
 static int proof_state_pp(lua_State * L) {
     int nargs = lua_gettop(L);
@@ -212,7 +211,6 @@ static const struct luaL_Reg proof_state_m[] = {
     {"pp",                   safe_function<proof_state_pp>},
     {"goals",                safe_function<proof_state_get_goals>},
     {"subst",                safe_function<proof_state_get_subst>},
-    {"initial",              safe_function<proof_state_get_initial>},
     {"ngen",                 safe_function<proof_state_get_ngen>},
     {"is_final_state",       safe_function<proof_state_is_final_state>},
     {0, 0}
diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h
index 49254437e..2b2e80362 100644
--- a/src/library/tactic/proof_state.h
+++ b/src/library/tactic/proof_state.h
@@ -18,24 +18,16 @@ class proof_state {
     goals            m_goals;
     substitution     m_subst;
     name_generator   m_ngen;
-    // The following term is of the form (?m l_1 ... l_n), it captures the
-    // metavariable this proof state is trying to synthesize, and
-    // the context [l_1, ..., l_n]. The context is important because it allows
-    // us to "reinterpret" an expression in this context.
-    expr             m_inital;
 public:
-    proof_state(goals const & gs, substitution const & s, name_generator const & ngen, expr const & ini):
-        m_goals(gs), m_subst(s), m_ngen(ngen), m_inital(ini) {}
-    proof_state(proof_state const & s, goals const & gs, substitution const & subst, name_generator const & ngen):
-        proof_state(gs, subst, ngen, s.m_inital) {}
-    proof_state(proof_state const & s, goals const & gs, substitution const & subst):proof_state(s, gs, subst, s.m_ngen) {}
+    proof_state(goals const & gs, substitution const & s, name_generator const & ngen):
+        m_goals(gs), m_subst(s), m_ngen(ngen) {}
+    proof_state(proof_state const & s, goals const & gs, substitution const & subst):proof_state(gs, subst, s.m_ngen) {}
     proof_state(proof_state const & s, goals const & gs):proof_state(s, gs, s.m_subst) {}
-    proof_state(proof_state const & s, name_generator const & ngen):proof_state(s.m_goals, s.m_subst, ngen, s.m_inital) {}
+    proof_state(proof_state const & s, name_generator const & ngen):proof_state(s.m_goals, s.m_subst, ngen) {}
 
     goals const & get_goals() const { return m_goals; }
     substitution const & get_subst() const { return m_subst; }
     name_generator const & get_ngen() const { return m_ngen; }
-    expr const & get_initial() const { return m_inital; }
 
     /** \brief Return true iff this state does not have any goals left */
     bool is_final_state() const { return empty(m_goals); }