diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp
index cd9618d03a..4df02852a4 100644
--- a/src/library/app_builder.cpp
+++ b/src/library/app_builder.cpp
@@ -16,7 +16,8 @@ Author: Leonardo de Moura
 
 namespace lean {
 struct app_builder::imp {
-    std::unique_ptr<tmp_type_context> m_ctx;
+    tmp_type_context * m_ctx;
+    bool               m_ctx_owner;
 
     struct entry {
         unsigned             m_num_umeta;
@@ -107,15 +108,26 @@ struct app_builder::imp {
     symm_info_getter  m_symm_getter;
     trans_info_getter m_trans_getter;
 
-    imp(std::unique_ptr<tmp_type_context> && ctx):
-        m_ctx(std::move(ctx)),
+    imp(tmp_type_context & ctx, bool owner):
+        m_ctx(&ctx),
+        m_ctx_owner(owner),
         m_refl_getter(mk_refl_info_getter(m_ctx->env())),
         m_symm_getter(mk_symm_info_getter(m_ctx->env())),
         m_trans_getter(mk_trans_info_getter(m_ctx->env())) {
     }
 
     imp(environment const & env, io_state const & ios, reducible_behavior b):
-        imp(std::unique_ptr<tmp_type_context>(new tmp_type_context(env, ios, b))) {
+        imp(*new tmp_type_context(env, ios, b), true) {
+    }
+
+    imp(tmp_type_context & ctx):
+        imp(ctx, false) {
+    }
+
+    ~imp() {
+        lean_assert(m_ctx);
+        if (m_ctx_owner)
+            delete m_ctx;
     }
 
     levels mk_metavars(declaration const & d, buffer<expr> & mvars, buffer<optional<expr>> & inst_args) {
@@ -445,8 +457,8 @@ app_builder::app_builder(environment const & env, reducible_behavior b):
     app_builder(env, get_dummy_ios(), b) {
 }
 
-app_builder::app_builder(std::unique_ptr<tmp_type_context> && ctx):
-    m_ptr(new imp(std::move(ctx))) {
+app_builder::app_builder(tmp_type_context & ctx):
+    m_ptr(new imp(ctx)) {
 }
 
 app_builder::~app_builder() {}
diff --git a/src/library/app_builder.h b/src/library/app_builder.h
index 76384fb64a..9e4922785a 100644
--- a/src/library/app_builder.h
+++ b/src/library/app_builder.h
@@ -32,8 +32,9 @@ class app_builder {
 public:
     app_builder(environment const & env, io_state const & ios, reducible_behavior b = UnfoldReducible);
     app_builder(environment const & env, reducible_behavior b = UnfoldReducible);
-    app_builder(std::unique_ptr<tmp_type_context> && ctx);
+    app_builder(tmp_type_context & ctx);
     ~app_builder();
+
     /** \brief Create an application (d.{_ ... _} _ ... _ args[0] ... args[nargs-1]).
         The missing arguments and universes levels are inferred using type inference.
 
@@ -108,7 +109,7 @@ public:
     /** \brief Set the local instances. This method is relevant when we want to expose local class instances
         to the app_builder.
 
-        \remark When the constructor app_builder(std::unique_ptr<tmp_type_context> && ctx) is used
+        \remark When the constructor app_builder(tmp_type_context & ctx) is used
         the initialization can be performed outside. */
     void set_local_instances(list<expr> const & insts);
 };