diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index bc47eaa78..0ff5c168e 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -281,14 +281,14 @@ struct environment::imp {
     /** \brief Add new axiom. */
     void add_axiom(name const & n, expr const & t, environment const & env) {
         check_name(n, env);
-        infer_universe(t, env);
+        m_type_checker.infer_universe(t);
         register_named_object(mk_axiom(n, t));
     }
 
     /** \brief Add new variable. */
     void add_var(name const & n, expr const & t, environment const & env) {
         check_name(n, env);
-        infer_universe(t, env);
+        m_type_checker.infer_universe(t);
         register_named_object(mk_var_decl(n, t));
     }
 
@@ -359,8 +359,8 @@ environment::environment():
 }
 
 // used when creating a new child environment
-environment::environment(imp * new_ptr):
-    m_imp(new_ptr) {
+environment::environment(std::shared_ptr<imp> const & parent, bool):
+    m_imp(new imp(parent, *this)) {
 }
 
 // used when creating a reference to the parent environment
@@ -372,7 +372,7 @@ environment::~environment() {
 }
 
 environment environment::mk_child() const {
-    return environment(new imp(m_imp, *this));
+    return environment(m_imp, true);
 }
 
 bool environment::has_children() const {
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index f216f3840..cdc86a943 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -21,6 +21,7 @@ private:
     struct imp;
     std::shared_ptr<imp> m_imp;
     void check_type(name const & n, expr const & t, expr const & v);
+    environment(std::shared_ptr<imp> const & parent, bool);
     explicit environment(std::shared_ptr<imp> const & ptr);
     explicit environment(imp * new_ptr);
     unsigned get_num_objects(bool local) const;
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index e55cba6d9..b83eac0e5 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -200,8 +200,4 @@ normalizer & type_checker::get_normalizer() { return m_ptr->get_normalizer(); }
 expr  infer_type(expr const & e, environment const & env, context const & ctx) {
     return type_checker(env).infer_type(e, ctx);
 }
-
-level infer_universe(expr const & t, environment const & env, context const & ctx) {
-    return type_checker(env).infer_universe(t, ctx);
-}
 }
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index 70a6066c8..5c87f5979 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -38,5 +38,4 @@ public:
 };
 
 expr infer_type(expr const & e, environment const & env, context const & ctx = context());
-level infer_universe(expr const & t, environment const & env, context const & ctx = context());
 }