diff --git a/src/library/tactic/change_tactic.cpp b/src/library/tactic/change_tactic.cpp
index 31aebe2d5a..c8d9a6ac12 100644
--- a/src/library/tactic/change_tactic.cpp
+++ b/src/library/tactic/change_tactic.cpp
@@ -18,9 +18,8 @@ vm_obj change_core(expr const & e, bool check, tactic_state const & s) {
         if (e == g->get_type()) return tactic::mk_success(s);
         type_context ctx         = mk_type_context_for(s);
         if (!check || ctx.is_def_eq(e, g->get_type())) {
-            auto mctx    = ctx.mctx();
-            expr new_e   = mctx.instantiate_mvars(e);
-            expr new_M   = mctx.mk_metavar_decl(g->get_context(), new_e);
+            expr new_e   = ctx.instantiate_mvars(e);
+            expr new_M   = ctx.mk_metavar_decl(g->get_context(), new_e);
             /*
                We use the proof term
 
@@ -29,6 +28,7 @@ vm_obj change_core(expr const & e, bool check, tactic_state const & s) {
                to create a "checkpoint". See discussion at issue #1260
             */
             expr  pr  = mk_id(ctx, g->get_type(), new_M);
+            auto mctx    = ctx.mctx();
             mctx.assign(head(s.goals()), pr);
             list<expr> new_gs(new_M, tail(s.goals()));
             return tactic::mk_success(set_mctx_goals(s, mctx, new_gs));