diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index fafe9d38f..1ab13b082 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -84,6 +84,7 @@ include_directories(${LEAN_SOURCE_DIR}/interval)
 include_directories(${LEAN_SOURCE_DIR}/kernel)
 include_directories(${LEAN_SOURCE_DIR}/library)
 include_directories(${LEAN_SOURCE_DIR}/library/arith)
+include_directories(${LEAN_SOURCE_DIR}/library/cast)
 include_directories(${LEAN_SOURCE_DIR}/library/import_all)
 include_directories(${LEAN_SOURCE_DIR}/parsers)
 include_directories(${LEAN_SOURCE_DIR}/frontends/lean)
@@ -102,6 +103,8 @@ add_subdirectory(library)
 set(LEAN_LIBS ${LEAN_LIBS} library)
 add_subdirectory(library/arith)
 set(LEAN_LIBS ${LEAN_LIBS} arithlib)
+add_subdirectory(library/cast)
+set(LEAN_LIBS ${LEAN_LIBS} castlib)
 add_subdirectory(library/import_all)
 set(LEAN_LIBS ${LEAN_LIBS} import_all)
 add_subdirectory(frontends/lean)
diff --git a/src/frontends/lean/lean_notation.cpp b/src/frontends/lean/lean_notation.cpp
index c7e357447..7df78dfb7 100644
--- a/src/frontends/lean/lean_notation.cpp
+++ b/src/frontends/lean/lean_notation.cpp
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "basic_thms.h"
 #include "lean_frontend.h"
 #include "arithlibs.h"
+#include "castlib.h"
 
 namespace lean {
 /**
diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index 570cee0f7..9499e6f51 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -141,99 +141,6 @@ public:
 MK_BUILTIN(if_fn, if_fn_value);
 // =======================================
 
-// =======================================
-// cast builtin operator
-static name   g_cast_name("Cast");
-static format g_cast_fmt(g_cast_name);
-expr mk_Cast_fn();
-class cast_fn_value : public value {
-    expr m_type;
-public:
-    cast_fn_value() {
-        expr A    = Const("A");
-        expr B    = Const("B");
-        // Cast: Pi (A : Type u) (B : Type u) (H : A = B) (a : A), B
-        m_type = Pi({{A, TypeU}, {B, TypeU}}, Eq(A,B) >> (A >> B));
-    }
-    virtual ~cast_fn_value() {}
-    virtual expr get_type() const { return m_type; }
-    virtual name get_name() const { return g_cast_name; }
-    virtual bool normalize(unsigned num_as, expr const * as, expr & r) const {
-        if (num_as > 4 && as[1] == as[2]) {
-            // Cast T T H a == a
-            if (num_as == 5)
-                r = as[4];
-            else
-                r = mk_app(num_as - 4, as + 4);
-            return true;
-        } else if (is_app(as[4]) &&
-                   arg(as[4], 0) == mk_Cast_fn() &&
-                   num_args(as[4]) == 5 &&
-                   as[1] == arg(as[4], 2)) {
-            // Cast T1 T2 H1 (Cast T3 T1 H2 a) == Cast T3 T2 (Trans H1 H2) a
-            expr const & nested = as[4];
-            expr const & T1 = as[1];
-            expr const & T2 = as[2];
-            expr const & T3 = arg(nested, 1);
-            expr const & H1 = as[3];
-            expr const & H2 = arg(nested, 3);
-            expr const & a  = arg(nested, 4);
-            expr c = Cast(T3, T2, Trans(TypeU, T3, T1, T2, H1, H2), a);
-            if (num_as == 5) {
-                r = c;
-            } else {
-                buffer<expr> new_as;
-                new_as.push_back(c);
-                new_as.append(num_as - 5, as + 5);
-                r = mk_app(new_as.size(), new_as.data());
-            }
-            return true;
-        } else if (num_as > 5 && is_pi(as[1]) && is_pi(as[2])) {
-            // cast T1 T2 H f a_1 ... a_k
-            // Propagate application over cast.
-            // Remark: we check if T1 is a Pi to prevent non-termination
-            // For example, H can be a bogus hypothesis that shows
-            // that A == A -> A
-
-            // Since T1 and T2 are Pi's, we decompose them
-            expr const & T1  = as[1]; // Pi x : A1, B1
-            expr const & T2  = as[2]; // Pi x : A2, B2
-            expr const & H   = as[3];
-            expr const & f   = as[4];
-            expr const & a_1 = as[5]; // has type A2
-            expr const & A1  = abst_domain(T1);
-            expr const & B1  = abst_body(T1);
-            expr const & A2  = abst_domain(T2);
-            expr const & B2  = abst_body(T2);
-            expr B1f         = mk_lambda(abst_name(T1), A1, B1);
-            expr B2f         = mk_lambda(abst_name(T2), A2, B2);
-            expr A1_eq_A2    = DomInj(A1, A2, B1f, B2f, H);
-            name t("t");
-            expr A2_eq_A1    = Symm(TypeU, A1, A2, A1_eq_A2);
-            expr a_1p        = Cast(A2, A1, A2_eq_A1, a_1);
-            expr fa_1        = f(a_1p);
-            // Cast fa_1 back to B2 since the type of cast T1 T2 H f a_1
-            // is in B2 a_1p
-            expr B1_eq_B2_at_a_1p = RanInj(A1, A2, B1f, B2f, H, a_1p);
-            expr fa_1_B2     = Cast(B1, B2, B1_eq_B2_at_a_1p, fa_1);
-            if (num_as == 6) {
-                r = fa_1_B2;
-            } else {
-                buffer<expr> new_as;
-                new_as.push_back(fa_1_B2);
-                new_as.append(num_as - 6, as + 6);
-                r = mk_app(new_as.size(), new_as.data());
-            }
-            return true;
-        } else {
-            return false;
-        }
-    }
-};
-MK_BUILTIN(Cast_fn, cast_fn_value);
-// =======================================
-
-
 MK_CONSTANT(implies_fn, name("implies"));
 MK_CONSTANT(iff_fn,     name("iff"));
 MK_CONSTANT(and_fn,     name("and"));
@@ -242,7 +149,6 @@ MK_CONSTANT(not_fn,     name("not"));
 MK_CONSTANT(forall_fn,  name("forall"));
 MK_CONSTANT(exists_fn,  name("exists"));
 MK_CONSTANT(homo_eq_fn, name("heq"));
-MK_CONSTANT(cast_fn,    name("cast"));
 
 // Axioms
 MK_CONSTANT(mp_fn,          name("MP"));
@@ -252,8 +158,6 @@ MK_CONSTANT(case_fn,        name("Case"));
 MK_CONSTANT(subst_fn,       name("Subst"));
 MK_CONSTANT(eta_fn,         name("Eta"));
 MK_CONSTANT(imp_antisym_fn, name("ImpAntisym"));
-MK_CONSTANT(dom_inj_fn,     name("DomInj"));
-MK_CONSTANT(ran_inj_fn,     name("RanInj"));
 
 // Basic theorems
 MK_CONSTANT(symm_fn,            name("Symm"));
@@ -273,13 +177,10 @@ void add_basic_theory(environment & env) {
     expr x         = Const("x");
     expr y         = Const("y");
     expr A         = Const("A");
-    expr Ap        = Const("A'");
     expr A_pred    = A >> Bool;
     expr B         = Const("B");
-    expr Bp        = Const("B'");
     expr q_type    = Pi({A, TypeU}, A_pred >> Bool);
     expr piABx     = Pi({x, A}, B(x));
-    expr piApBpx   = Pi({x, Ap}, Bp(x));
     expr A_arrow_u = A >> TypeU;
     expr P         = Const("P");
     expr H         = Const("H");
@@ -290,7 +191,6 @@ void add_basic_theory(environment & env) {
     env.add_builtin(mk_bool_value(true));
     env.add_builtin(mk_bool_value(false));
     env.add_builtin(mk_if_fn());
-    env.add_builtin(mk_Cast_fn());
 
     // implies(x, y) := if x y True
     env.add_definition(implies_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, True)));
@@ -315,10 +215,6 @@ void add_basic_theory(environment & env) {
     // homogeneous equality
     env.add_definition(homo_eq_fn_name, Pi({{A,TypeU},{x,A},{y,A}}, Bool), Fun({{A,TypeU}, {x,A}, {y,A}}, Eq(x, y)));
 
-    // Alias for Cast operator. We create the alias to be able to mark
-    // implicit arguments.
-    env.add_definition(cast_fn_name, Pi({{A, TypeU}, {B, TypeU}}, Eq(A,B) >> (A >> B)), mk_Cast_fn());
-
     // MP : Pi (a b : Bool) (H1 : a => b) (H2 : a), b
     env.add_axiom(mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, a}}, b));
 
@@ -340,14 +236,6 @@ void add_basic_theory(environment & env) {
     // ImpliesAntisym : Pi (a b : Bool) (H1 : a => b) (H2 : b => a), a = b
     env.add_axiom(imp_antisym_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Implies(b, a)}}, Eq(a, b)));
 
-    // DomInj : Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)), A = A'
-    env.add_axiom(dom_inj_fn_name, Pi({{A, TypeU}, {Ap, TypeU}, {B, A >> TypeU}, {Bp, Ap >> TypeU}, {H, Eq(piABx, piApBpx)}}, Eq(A, Ap)));
-
-    // RanInj : Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A),
-    //                     B a = B' (cast A A' (DomInj A A' B B' H) a)
-    env.add_axiom(ran_inj_fn_name, Pi({{A, TypeU}, {Ap, TypeU}, {B, A >> TypeU}, {Bp, Ap >> TypeU}, {H, Eq(piABx, piApBpx)}, {a, A}},
-                                      Eq(B(a), Bp(Cast(A, Ap, DomInj(A, Ap, B, Bp, H), a)))));
-
     // Symm : Pi (A : Type u) (a b : A) (H : a = b), b = a
     env.add_theorem(symm_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}}, Eq(b, a)),
                     Fun({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}},
diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h
index bab09ef62..235b05361 100644
--- a/src/kernel/builtin.h
+++ b/src/kernel/builtin.h
@@ -113,12 +113,6 @@ expr mk_homo_eq_fn();
 inline expr mk_homo_eq(expr const & A, expr const & l, expr const & r) { return mk_app(mk_homo_eq_fn(), A, l, r); }
 inline expr hEq(expr const & A, expr const & l, expr const & r) { return mk_homo_eq(A, l, r); }
 
-/** \brief Type Cast. It has type <tt>Pi (A : Type u) (B : Type u) (H : A = B) (a : A), B</tt> */
-expr mk_cast_fn();
-/** \brief Return the term (cast A B H a) */
-inline expr mk_cast(expr const & A, expr const & B, expr const & H, expr const & a) { return mk_app(mk_cast_fn(), A, B, H, a); }
-inline expr Cast(expr const & A, expr const & B, expr const & H, expr const & a) { return mk_cast(A, B, H, a); }
-
 /** \brief Modus Ponens axiom */
 expr mk_mp_fn();
 /** \brief (Axiom) {a : Bool}, {b : Bool}, H1 : a => b, H2 : a |- MP(a, b, H1, H2) : b */
@@ -154,20 +148,6 @@ expr mk_imp_antisym_fn();
 /** \brief (Axiom) {a : Bool}, {b : Bool}, H1 : a => b, H2 : b => a |- ImpAntisym(a, b, H1, H2) : a = b */
 inline expr ImpAntisym(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_imp_antisym_fn(), a, b, H1, H2); }
 
-/** \brief Domain Injectivity. It has type <tt>Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)), A = A' </tt> */
-expr mk_dom_inj_fn();
-/** \brief Return the term (DomInj A A' B B' H) */
-inline expr mk_dom_inj(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H) { return mk_app({mk_dom_inj_fn(), A, Ap, B, Bp, H}); }
-inline expr DomInj(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H) { return mk_dom_inj(A, Ap, B, Bp, H); }
-
-/** \brief Range Injectivity. It has type <tt>Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A),
-                                                 B a = B' (cast A A' (DomInj A A' B B' H) a)</tt>
-*/
-expr mk_ran_inj_fn();
-/** \brief Return the term (RanInj A A' B B' H) */
-inline expr mk_ran_inj(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H, expr const & a) { return mk_app({mk_ran_inj_fn(), A, Ap, B, Bp, H, a}); }
-inline expr RanInj(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H, expr const & a) { return mk_ran_inj(A, Ap, B, Bp, H, a); }
-
 expr mk_symm_fn();
 /** \brief (Theorem) {A : Type u}, {a b : A}, H : a = b |- Symm(A, a, b, H) : b = a */
 inline expr Symm(expr const & A, expr const & a, expr const & b, expr const & H) { return mk_app(mk_symm_fn(), A, a, b, H); }
diff --git a/src/library/cast/CMakeLists.txt b/src/library/cast/CMakeLists.txt
new file mode 100644
index 000000000..30dce5773
--- /dev/null
+++ b/src/library/cast/CMakeLists.txt
@@ -0,0 +1,2 @@
+add_library(castlib castlib.cpp)
+target_link_libraries(castlib ${LEAN_LIBS})
diff --git a/src/library/cast/castlib.cpp b/src/library/cast/castlib.cpp
new file mode 100644
index 000000000..9793ef642
--- /dev/null
+++ b/src/library/cast/castlib.cpp
@@ -0,0 +1,134 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "castlib.h"
+#include "environment.h"
+#include "abstract.h"
+#include "builtin.h"
+
+namespace lean {
+// Cast builtin operator
+static name   g_cast_name("Cast");
+static format g_cast_fmt(g_cast_name);
+expr mk_Cast_fn();
+class cast_fn_value : public value {
+    expr m_type;
+public:
+    cast_fn_value() {
+        expr A    = Const("A");
+        expr B    = Const("B");
+        // Cast: Pi (A : Type u) (B : Type u) (H : A = B) (a : A), B
+        m_type = Pi({{A, TypeU}, {B, TypeU}}, Eq(A,B) >> (A >> B));
+    }
+    virtual ~cast_fn_value() {}
+    virtual expr get_type() const { return m_type; }
+    virtual name get_name() const { return g_cast_name; }
+    virtual bool normalize(unsigned num_as, expr const * as, expr & r) const {
+        if (num_as > 4 && as[1] == as[2]) {
+            // Cast T T H a == a
+            if (num_as == 5)
+                r = as[4];
+            else
+                r = mk_app(num_as - 4, as + 4);
+            return true;
+        } else if (is_app(as[4]) &&
+                   arg(as[4], 0) == mk_Cast_fn() &&
+                   num_args(as[4]) == 5 &&
+                   as[1] == arg(as[4], 2)) {
+            // Cast T1 T2 H1 (Cast T3 T1 H2 a) == Cast T3 T2 (Trans H1 H2) a
+            expr const & nested = as[4];
+            expr const & T1 = as[1];
+            expr const & T2 = as[2];
+            expr const & T3 = arg(nested, 1);
+            expr const & H1 = as[3];
+            expr const & H2 = arg(nested, 3);
+            expr const & a  = arg(nested, 4);
+            expr c = Cast(T3, T2, Trans(TypeU, T3, T1, T2, H1, H2), a);
+            if (num_as == 5) {
+                r = c;
+            } else {
+                buffer<expr> new_as;
+                new_as.push_back(c);
+                new_as.append(num_as - 5, as + 5);
+                r = mk_app(new_as.size(), new_as.data());
+            }
+            return true;
+        } else if (num_as > 5 && is_pi(as[1]) && is_pi(as[2])) {
+            // cast T1 T2 H f a_1 ... a_k
+            // Propagate application over cast.
+            // Remark: we check if T1 is a Pi to prevent non-termination
+            // For example, H can be a bogus hypothesis that shows
+            // that A == A -> A
+
+            // Since T1 and T2 are Pi's, we decompose them
+            expr const & T1  = as[1]; // Pi x : A1, B1
+            expr const & T2  = as[2]; // Pi x : A2, B2
+            expr const & H   = as[3];
+            expr const & f   = as[4];
+            expr const & a_1 = as[5]; // has type A2
+            expr const & A1  = abst_domain(T1);
+            expr const & B1  = abst_body(T1);
+            expr const & A2  = abst_domain(T2);
+            expr const & B2  = abst_body(T2);
+            expr B1f         = mk_lambda(abst_name(T1), A1, B1);
+            expr B2f         = mk_lambda(abst_name(T2), A2, B2);
+            expr A1_eq_A2    = DomInj(A1, A2, B1f, B2f, H);
+            name t("t");
+            expr A2_eq_A1    = Symm(TypeU, A1, A2, A1_eq_A2);
+            expr a_1p        = Cast(A2, A1, A2_eq_A1, a_1);
+            expr fa_1        = f(a_1p);
+            // Cast fa_1 back to B2 since the type of cast T1 T2 H f a_1
+            // is in B2 a_1p
+            expr B1_eq_B2_at_a_1p = RanInj(A1, A2, B1f, B2f, H, a_1p);
+            expr fa_1_B2     = Cast(B1, B2, B1_eq_B2_at_a_1p, fa_1);
+            if (num_as == 6) {
+                r = fa_1_B2;
+            } else {
+                buffer<expr> new_as;
+                new_as.push_back(fa_1_B2);
+                new_as.append(num_as - 6, as + 6);
+                r = mk_app(new_as.size(), new_as.data());
+            }
+            return true;
+        } else {
+            return false;
+        }
+    }
+};
+MK_BUILTIN(Cast_fn,     cast_fn_value);
+MK_CONSTANT(cast_fn,    name("cast"));
+MK_CONSTANT(dom_inj_fn, name("DomInj"));
+MK_CONSTANT(ran_inj_fn, name("RanInj"));
+
+void import_castlib(environment & env) {
+    if (env.find_object(to_value(mk_Cast_fn()).get_name()))
+        return;
+    expr x         = Const("x");
+    expr A         = Const("A");
+    expr Ap        = Const("A'");
+    expr B         = Const("B");
+    expr Bp        = Const("B'");
+    expr piABx     = Pi({x, A}, B(x));
+    expr piApBpx   = Pi({x, Ap}, Bp(x));
+    expr H         = Const("H");
+    expr a         = Const("a");
+    expr b         = Const("b");
+
+    env.add_builtin(mk_Cast_fn());
+
+    // Alias for Cast operator. We create the alias to be able to mark
+    // implicit arguments.
+    env.add_definition(cast_fn_name, Pi({{A, TypeU}, {B, TypeU}}, Eq(A,B) >> (A >> B)), mk_Cast_fn());
+
+    // DomInj : Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)), A = A'
+    env.add_axiom(dom_inj_fn_name, Pi({{A, TypeU}, {Ap, TypeU}, {B, A >> TypeU}, {Bp, Ap >> TypeU}, {H, Eq(piABx, piApBpx)}}, Eq(A, Ap)));
+
+    // RanInj : Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A),
+    //                     B a = B' (cast A A' (DomInj A A' B B' H) a)
+    env.add_axiom(ran_inj_fn_name, Pi({{A, TypeU}, {Ap, TypeU}, {B, A >> TypeU}, {Bp, Ap >> TypeU}, {H, Eq(piABx, piApBpx)}, {a, A}},
+                                      Eq(B(a), Bp(Cast(A, Ap, DomInj(A, Ap, B, Bp, H), a)))));
+}
+}
diff --git a/src/library/cast/castlib.h b/src/library/cast/castlib.h
new file mode 100644
index 000000000..715f41614
--- /dev/null
+++ b/src/library/cast/castlib.h
@@ -0,0 +1,45 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "expr.h"
+
+namespace lean {
+/** \brief Type Cast. It has type <tt>Pi (A : Type u) (B : Type u) (H : A = B) (a : A), B</tt> */
+expr mk_cast_fn();
+/** \brief Return the term (cast A B H a) */
+inline expr mk_cast(expr const & A, expr const & B, expr const & H, expr const & a) { return mk_app(mk_cast_fn(), A, B, H, a); }
+inline expr Cast(expr const & A, expr const & B, expr const & H, expr const & a) { return mk_cast(A, B, H, a); }
+
+/** \brief Domain Injectivity.
+    It has type <tt>Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)), A = A' </tt>
+*/
+expr mk_dom_inj_fn();
+/** \brief Return the term (DomInj A A' B B' H) */
+inline expr mk_dom_inj(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H) {
+    return mk_app({mk_dom_inj_fn(), A, Ap, B, Bp, H});
+}
+inline expr DomInj(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H) {
+    return mk_dom_inj(A, Ap, B, Bp, H);
+}
+
+/** \brief Range Injectivity.
+    It has type <tt>Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A),
+                       B a = B' (cast A A' (DomInj A A' B B' H) a)</tt>
+*/
+expr mk_ran_inj_fn();
+/** \brief Return the term (RanInj A A' B B' H) */
+inline expr mk_ran_inj(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H, expr const & a) {
+    return mk_app({mk_ran_inj_fn(), A, Ap, B, Bp, H, a});
+}
+inline expr RanInj(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H, expr const & a) {
+    return mk_ran_inj(A, Ap, B, Bp, H, a);
+}
+
+class environment;
+/** \brief Import type "casting" library */
+void import_castlib(environment & env);
+}
diff --git a/src/library/import_all/import_all.cpp b/src/library/import_all/import_all.cpp
index 83ddb81c3..e0a67acc7 100644
--- a/src/library/import_all/import_all.cpp
+++ b/src/library/import_all/import_all.cpp
@@ -8,12 +8,14 @@ Author: Leonardo de Moura
 #include "builtin.h"
 #include "basic_thms.h"
 #include "arithlibs.h"
+#include "castlib.h"
 
 namespace lean {
 void import_all(environment & env) {
     add_basic_theory(env);
     add_basic_thms(env);
     import_arithlibs(env);
+    import_castlib(env);
 }
 environment mk_toplevel() {
     environment r;
diff --git a/src/tests/kernel/threads.cpp b/src/tests/kernel/threads.cpp
index 392dba177..613351114 100644
--- a/src/tests/kernel/threads.cpp
+++ b/src/tests/kernel/threads.cpp
@@ -18,8 +18,7 @@ Author: Leonardo de Moura
 #include "test.h"
 using namespace lean;
 
-expr normalize(expr const & e) {
-    environment env = mk_toplevel();
+expr norm(expr const & e, environment & env) {
     env.add_var("a", Int);
     env.add_var("b", Int);
     env.add_var("f", Int >> (Int >> Int));
@@ -28,6 +27,7 @@ expr normalize(expr const & e) {
 }
 
 static void mk(expr const & a) {
+    environment env = mk_toplevel();
     expr b = Const("b");
     for (unsigned i = 0; i < 100; i++) {
         expr h = Const("h");
@@ -36,7 +36,8 @@ static void mk(expr const & a) {
             h = mk_app(h, b);
         h = max_sharing(h);
         lean_assert(closed(h));
-        h = normalize(h);
+        environment env2 = env.mk_child();
+        h = norm(h, env2);
         h = abstract(h, a);
         lean_assert(!closed(h));
         h = deep_copy(h);