diff --git a/src/library/unfold_macros.cpp b/src/library/unfold_macros.cpp
index 2367445b0..668bb514c 100644
--- a/src/library/unfold_macros.cpp
+++ b/src/library/unfold_macros.cpp
@@ -110,8 +110,8 @@ public:
     expr operator()(expr const & e) { return visit(e); }
 };
 
-static bool contains_untrusted_macro(environment const & env, unsigned trust_lvl, expr const & e) {
-    if (env.trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL)
+static bool contains_untrusted_macro(unsigned trust_lvl, expr const & e) {
+    if (trust_lvl > LEAN_BELIEVER_TRUST_LEVEL)
         return false;
     return static_cast<bool>(find(e, [&](expr const & e, unsigned) {
                 return is_macro(e) && macro_def(e).trust_level() >= trust_lvl;
@@ -119,7 +119,7 @@ static bool contains_untrusted_macro(environment const & env, unsigned trust_lvl
 }
 
 expr unfold_untrusted_macros(environment const & env, expr const & e, unsigned trust_lvl) {
-    if (contains_untrusted_macro(env, trust_lvl, e)) {
+    if (contains_untrusted_macro(trust_lvl, e)) {
         return unfold_untrusted_macros_fn(env, trust_lvl)(e);
     } else {
         return e;
@@ -134,16 +134,16 @@ expr unfold_all_macros(environment const & env, expr const & e) {
     return unfold_untrusted_macros(env, e, 0);
 }
 
-static bool contains_untrusted_macro(environment const & env, unsigned trust_lvl, declaration const & d) {
-    if (env.trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL)
+static bool contains_untrusted_macro(unsigned trust_lvl, declaration const & d) {
+    if (trust_lvl > LEAN_BELIEVER_TRUST_LEVEL)
         return false;
-    if (contains_untrusted_macro(env, trust_lvl, d.get_type()))
+    if (contains_untrusted_macro(trust_lvl, d.get_type()))
         return true;
-    return (d.is_definition() || d.is_theorem()) && contains_untrusted_macro(env, trust_lvl, d.get_value());
+    return (d.is_definition() || d.is_theorem()) && contains_untrusted_macro(trust_lvl, d.get_value());
 }
 
 declaration unfold_untrusted_macros(environment const & env, declaration const & d, unsigned trust_lvl) {
-    if (contains_untrusted_macro(env, trust_lvl, d)) {
+    if (contains_untrusted_macro(trust_lvl, d)) {
         expr new_t = unfold_untrusted_macros(env, d.get_type(), trust_lvl);
         if (d.is_theorem()) {
             expr new_v = unfold_untrusted_macros(env, d.get_value(), trust_lvl);
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index ccef8ec13..20783109b 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -26,6 +26,7 @@ add_test(lean_ghash1   "${CMAKE_CURRENT_BINARY_DIR}/lean" -g)
 add_test(lean_ghash2   "${CMAKE_CURRENT_BINARY_DIR}/lean" --githash)
 add_test(lean_path1    "${CMAKE_CURRENT_BINARY_DIR}/lean" -p)
 add_test(lean_path2    "${CMAKE_CURRENT_BINARY_DIR}/lean" --path)
+add_test(export_all    "${LEAN_SOURCE_DIR}/../bin/lean" --export-all=all.out "${LEAN_SOURCE_DIR}/../library/standard.lean")
 add_test(lean_luahook1 "${CMAKE_CURRENT_BINARY_DIR}/lean" --luahook=100 "${LEAN_SOURCE_DIR}/../tests/lua/big.lua")
 add_test(lean_luahook2 "${CMAKE_CURRENT_BINARY_DIR}/lean" -k 100 "${LEAN_SOURCE_DIR}/../tests/lua/big.lua")
 # add_test(lean_lua1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "--lua" "${LEAN_SOURCE_DIR}/../tests/lua/single.lua")