diff --git a/src/frontends/lean/coercion.cpp b/src/frontends/lean/coercion.cpp
index 7c3b65873..1c76b7fa0 100644
--- a/src/frontends/lean/coercion.cpp
+++ b/src/frontends/lean/coercion.cpp
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "library/io_state_stream.h"
 #include "frontends/lean/coercion.h"
 #include "frontends/lean/frontend.h"
 
diff --git a/src/frontends/lean/environment_scope.cpp b/src/frontends/lean/environment_scope.cpp
index aec93e41e..c74387127 100644
--- a/src/frontends/lean/environment_scope.cpp
+++ b/src/frontends/lean/environment_scope.cpp
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "kernel/replace_fn.h"
 #include "kernel/abstract.h"
+#include "library/io_state_stream.h"
 #include "frontends/lean/frontend.h"
 
 namespace lean {
diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp
index e8fb075c8..098dc5ca7 100644
--- a/src/frontends/lean/frontend.cpp
+++ b/src/frontends/lean/frontend.cpp
@@ -19,6 +19,7 @@ Author: Leonardo de Moura
 #include "kernel/expr_sets.h"
 #include "kernel/builtin.h"
 #include "kernel/io_state.h"
+#include "library/io_state_stream.h"
 #include "library/expr_pair.h"
 #include "library/expr_pair_maps.h"
 #include "library/arith/nat.h"
diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp
index b53e7897b..e5b9dcca5 100644
--- a/src/frontends/lean/frontend_elaborator.cpp
+++ b/src/frontends/lean/frontend_elaborator.cpp
@@ -17,6 +17,7 @@ Author: Leonardo de Moura
 #include "kernel/unification_constraint.h"
 #include "kernel/instantiate.h"
 #include "kernel/builtin.h"
+#include "library/io_state_stream.h"
 #include "library/placeholder.h"
 #include "library/elaborator/elaborator.h"
 #include "frontends/lean/frontend.h"
diff --git a/src/frontends/lean/operator_info.cpp b/src/frontends/lean/operator_info.cpp
index a488a7ffd..9d8dba01c 100644
--- a/src/frontends/lean/operator_info.cpp
+++ b/src/frontends/lean/operator_info.cpp
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/rc.h"
+#include "library/io_state_stream.h"
 #include "frontends/lean/operator_info.h"
 #include "frontends/lean/frontend.h"
 
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 976e8357a..c21383fc5 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "library/io_state_stream.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/pp.h"
 #include "frontends/lean/parser_imp.h"
diff --git a/src/frontends/lean/parser_calc.cpp b/src/frontends/lean/parser_calc.cpp
index ea9eb7718..3868b0457 100644
--- a/src/frontends/lean/parser_calc.cpp
+++ b/src/frontends/lean/parser_calc.cpp
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "kernel/builtin.h"
 #include "library/placeholder.h"
+#include "library/io_state_stream.h"
 #include "frontends/lean/parser_calc.h"
 #include "frontends/lean/parser_imp.h"
 #include "frontends/lean/operator_info.h"
diff --git a/src/frontends/lean/parser_cmds.cpp b/src/frontends/lean/parser_cmds.cpp
index b836d27ca..7dcfc5540 100644
--- a/src/frontends/lean/parser_cmds.cpp
+++ b/src/frontends/lean/parser_cmds.cpp
@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "kernel/normalizer.h"
 #include "kernel/type_checker.h"
 #include "library/placeholder.h"
+#include "library/io_state_stream.h"
 #include "frontends/lean/parser_imp.h"
 #include "frontends/lean/frontend.h"
 #include "frontends/lean/pp.h"
diff --git a/src/frontends/lean/parser_error.cpp b/src/frontends/lean/parser_error.cpp
index 3a4739f7a..5cecc64b8 100644
--- a/src/frontends/lean/parser_error.cpp
+++ b/src/frontends/lean/parser_error.cpp
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <utility>
 #include "kernel/kernel_exception.h"
+#include "library/io_state_stream.h"
 #include "frontends/lean/parser_imp.h"
 
 namespace lean {
diff --git a/src/frontends/lean/parser_expr.cpp b/src/frontends/lean/parser_expr.cpp
index 1d96ee917..6023717d0 100644
--- a/src/frontends/lean/parser_expr.cpp
+++ b/src/frontends/lean/parser_expr.cpp
@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "kernel/free_vars.h"
 #include "kernel/builtin.h"
 #include "library/placeholder.h"
+#include "library/io_state_stream.h"
 #include "library/arith/nat.h"
 #include "library/arith/int.h"
 #include "library/arith/real.h"
diff --git a/src/frontends/lean/parser_imp.cpp b/src/frontends/lean/parser_imp.cpp
index 577f185de..d6b53ac32 100644
--- a/src/frontends/lean/parser_imp.cpp
+++ b/src/frontends/lean/parser_imp.cpp
@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include <utility>
 #include <string>
 #include <vector>
+#include "library/io_state_stream.h"
 #include "frontends/lean/parser_imp.h"
 #include "frontends/lean/parser_macros.h"
 #include "frontends/lean/parser_calc.h"
diff --git a/src/frontends/lean/parser_level.cpp b/src/frontends/lean/parser_level.cpp
index 00ffb0c9a..2db323683 100644
--- a/src/frontends/lean/parser_level.cpp
+++ b/src/frontends/lean/parser_level.cpp
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "library/io_state_stream.h"
 #include "frontends/lean/parser_imp.h"
 namespace lean {
 // ==========================================
diff --git a/src/frontends/lean/parser_macros.cpp b/src/frontends/lean/parser_macros.cpp
index bb7311aa7..5f8bd725e 100644
--- a/src/frontends/lean/parser_macros.cpp
+++ b/src/frontends/lean/parser_macros.cpp
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "library/io_state_stream.h"
 #include "frontends/lean/parser_imp.h"
 #include "frontends/lean/notation.h"
 
diff --git a/src/frontends/lean/parser_tactic.cpp b/src/frontends/lean/parser_tactic.cpp
index 2a183026a..5c5ea9880 100644
--- a/src/frontends/lean/parser_tactic.cpp
+++ b/src/frontends/lean/parser_tactic.cpp
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "kernel/type_checker_justification.h"
 #include "kernel/unification_constraint.h"
+#include "library/io_state_stream.h"
 #include "library/expr_lt.h"
 #include "library/elaborator/elaborator.h"
 #include "frontends/lean/parser_imp.h"
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index e320abc9b..c9f6bf963 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -23,6 +23,7 @@ Author: Leonardo de Moura
 #include "kernel/replace_fn.h"
 #include "library/context_to_lambda.h"
 #include "library/placeholder.h"
+#include "library/io_state_stream.h"
 #include "frontends/lean/notation.h"
 #include "frontends/lean/pp.h"
 #include "frontends/lean/frontend.h"
diff --git a/src/frontends/lean/register_module.cpp b/src/frontends/lean/register_module.cpp
index 9acf85bdd..f56d9d5b7 100644
--- a/src/frontends/lean/register_module.cpp
+++ b/src/frontends/lean/register_module.cpp
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "util/sexpr/options.h"
 #include "kernel/io_state.h"
 #include "library/kernel_bindings.h"
+#include "library/io_state_stream.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/frontend.h"
 #include "frontends/lean/pp.h"
diff --git a/src/frontends/lua/register_modules.cpp b/src/frontends/lua/register_modules.cpp
index fed9a2c6f..3218718f4 100644
--- a/src/frontends/lua/register_modules.cpp
+++ b/src/frontends/lua/register_modules.cpp
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "util/numerics/register_module.h"
 #include "util/sexpr/register_module.h"
 #include "library/register_module.h"
+#include "library/io_state_stream.h"
 #include "library/arith/register_module.h"
 #include "library/tactic/register_module.h"
 #include "frontends/lean/register_module.h"
diff --git a/src/kernel/io_state.cpp b/src/kernel/io_state.cpp
index 1ec5872a7..11c660be3 100644
--- a/src/kernel/io_state.cpp
+++ b/src/kernel/io_state.cpp
@@ -40,33 +40,4 @@ void io_state::set_options(options const & opts) {
 void io_state::set_formatter(formatter const & f) {
     m_formatter = f;
 }
-
-io_state_stream const & operator<<(io_state_stream const & out, endl_class) {
-    out.get_stream() << std::endl;
-    return out;
-}
-
-io_state_stream const & operator<<(io_state_stream const & out, expr const & e) {
-    options const & opts = out.get_options();
-    out.get_stream() << mk_pair(out.get_formatter()(e, opts), opts);
-    return out;
-}
-
-io_state_stream const & operator<<(io_state_stream const & out, object const & obj) {
-    options const & opts = out.get_options();
-    out.get_stream() << mk_pair(out.get_formatter()(obj, opts), opts);
-    return out;
-}
-
-io_state_stream const & operator<<(io_state_stream const & out, environment const & env) {
-    options const & opts = out.get_options();
-    out.get_stream() << mk_pair(out.get_formatter()(env, opts), opts);
-    return out;
-}
-
-io_state_stream const & operator<<(io_state_stream const & out, kernel_exception const & ex) {
-    options const & opts = out.get_options();
-    out.get_stream() << mk_pair(ex.pp(out.get_formatter(), opts), opts);
-    return out;
-}
 }
diff --git a/src/kernel/io_state.h b/src/kernel/io_state.h
index 307aa7e3b..ac15c9387 100644
--- a/src/kernel/io_state.h
+++ b/src/kernel/io_state.h
@@ -40,54 +40,4 @@ public:
         set_options(get_options().update(n, v));
     }
 };
-
-/**
-   \brief Base class for \c regular and \c diagnostic wrapper classes.
-*/
-class io_state_stream {
-protected:
-    io_state const & m_io_state;
-public:
-    io_state_stream(io_state const & s):m_io_state(s) {}
-    virtual std::ostream & get_stream() const = 0;
-    void flush() { get_stream().flush(); }
-    formatter get_formatter() const { return m_io_state.get_formatter(); }
-    options get_options() const { return m_io_state.get_options(); }
-};
-
-/**
-   \brief Wrapper for the io_state object that provides access to the
-   io_state's regular channel
-*/
-class regular : public io_state_stream {
-public:
-    regular(io_state const & s):io_state_stream(s) {}
-    std::ostream & get_stream() const { return m_io_state.get_regular_channel().get_stream(); }
-};
-
-/**
-   \brief Wrapper for the io_state object that provides access to the
-   io_state's diagnostic channel
-*/
-class diagnostic : public io_state_stream {
-public:
-    diagnostic(io_state const & s):io_state_stream(s) {}
-    std::ostream & get_stream() const { return m_io_state.get_diagnostic_channel().get_stream(); }
-};
-
-// hack for using std::endl with channels
-struct endl_class { endl_class() {} };
-const endl_class endl;
-
-class kernel_exception;
-
-io_state_stream const & operator<<(io_state_stream const & out, endl_class);
-io_state_stream const & operator<<(io_state_stream const & out, expr const & e);
-io_state_stream const & operator<<(io_state_stream const & out, object const & obj);
-io_state_stream const & operator<<(io_state_stream const & out, environment const & env);
-io_state_stream const & operator<<(io_state_stream const & out, kernel_exception const & ex);
-template<typename T> io_state_stream const & operator<<(io_state_stream const & out, T const & t) {
-    out.get_stream() << t;
-    return out;
-}
 }
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index a3733efbd..1a472aa9f 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -1,5 +1,5 @@
 add_library(library kernel_bindings.cpp deep_copy.cpp max_sharing.cpp
   context_to_lambda.cpp placeholder.cpp expr_lt.cpp substitution.cpp
-  fo_unify.cpp bin_op.cpp eq_heq.cpp)
+  fo_unify.cpp bin_op.cpp eq_heq.cpp io_state_stream.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})
diff --git a/src/library/io_state_stream.cpp b/src/library/io_state_stream.cpp
new file mode 100644
index 000000000..a3b1527ab
--- /dev/null
+++ b/src/library/io_state_stream.cpp
@@ -0,0 +1,38 @@
+/*
+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 "library/io_state_stream.h"
+#include "kernel/kernel_exception.h"
+namespace lean {
+io_state_stream const & operator<<(io_state_stream const & out, endl_class) {
+    out.get_stream() << std::endl;
+    return out;
+}
+
+io_state_stream const & operator<<(io_state_stream const & out, expr const & e) {
+    options const & opts = out.get_options();
+    out.get_stream() << mk_pair(out.get_formatter()(e, opts), opts);
+    return out;
+}
+
+io_state_stream const & operator<<(io_state_stream const & out, object const & obj) {
+    options const & opts = out.get_options();
+    out.get_stream() << mk_pair(out.get_formatter()(obj, opts), opts);
+    return out;
+}
+
+io_state_stream const & operator<<(io_state_stream const & out, environment const & env) {
+    options const & opts = out.get_options();
+    out.get_stream() << mk_pair(out.get_formatter()(env, opts), opts);
+    return out;
+}
+
+io_state_stream const & operator<<(io_state_stream const & out, kernel_exception const & ex) {
+    options const & opts = out.get_options();
+    out.get_stream() << mk_pair(ex.pp(out.get_formatter(), opts), opts);
+    return out;
+}
+}
diff --git a/src/library/io_state_stream.h b/src/library/io_state_stream.h
new file mode 100644
index 000000000..9002b345b
--- /dev/null
+++ b/src/library/io_state_stream.h
@@ -0,0 +1,60 @@
+/*
+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 "kernel/io_state.h"
+
+namespace lean {
+/**
+   \brief Base class for \c regular and \c diagnostic wrapper classes.
+*/
+class io_state_stream {
+protected:
+    io_state const & m_io_state;
+public:
+    io_state_stream(io_state const & s):m_io_state(s) {}
+    virtual std::ostream & get_stream() const = 0;
+    void flush() { get_stream().flush(); }
+    formatter get_formatter() const { return m_io_state.get_formatter(); }
+    options get_options() const { return m_io_state.get_options(); }
+};
+
+/**
+   \brief Wrapper for the io_state object that provides access to the
+   io_state's regular channel
+*/
+class regular : public io_state_stream {
+public:
+    regular(io_state const & s):io_state_stream(s) {}
+    std::ostream & get_stream() const { return m_io_state.get_regular_channel().get_stream(); }
+};
+
+/**
+   \brief Wrapper for the io_state object that provides access to the
+   io_state's diagnostic channel
+*/
+class diagnostic : public io_state_stream {
+public:
+    diagnostic(io_state const & s):io_state_stream(s) {}
+    std::ostream & get_stream() const { return m_io_state.get_diagnostic_channel().get_stream(); }
+};
+
+// hack for using std::endl with channels
+struct endl_class { endl_class() {} };
+const endl_class endl;
+
+class kernel_exception;
+
+io_state_stream const & operator<<(io_state_stream const & out, endl_class);
+io_state_stream const & operator<<(io_state_stream const & out, expr const & e);
+io_state_stream const & operator<<(io_state_stream const & out, object const & obj);
+io_state_stream const & operator<<(io_state_stream const & out, environment const & env);
+io_state_stream const & operator<<(io_state_stream const & out, kernel_exception const & ex);
+template<typename T> io_state_stream const & operator<<(io_state_stream const & out, T const & t) {
+    out.get_stream() << t;
+    return out;
+}
+}
diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index f8fb5bbb2..78d05a924 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -20,6 +20,7 @@ Author: Leonardo de Moura
 #include "kernel/builtin.h"
 #include "kernel/io_state.h"
 #include "kernel/type_checker.h"
+#include "library/io_state_stream.h"
 #include "library/expr_lt.h"
 #include "library/kernel_bindings.h"
 
diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp
index b26645a56..daa73825a 100644
--- a/src/library/tactic/apply_tactic.cpp
+++ b/src/library/tactic/apply_tactic.cpp
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "kernel/abstract.h"
 #include "kernel/replace_visitor.h"
+#include "library/io_state_stream.h"
 #include "library/fo_unify.h"
 #include "library/placeholder.h"
 #include "library/kernel_bindings.h"
diff --git a/src/library/tactic/boolean_tactics.cpp b/src/library/tactic/boolean_tactics.cpp
index 0fafb5ec0..6ce632848 100644
--- a/src/library/tactic/boolean_tactics.cpp
+++ b/src/library/tactic/boolean_tactics.cpp
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/builtin.h"
 #include "kernel/abstract.h"
 #include "kernel/occurs.h"
+#include "library/io_state_stream.h"
 #include "library/tactic/goal.h"
 #include "library/tactic/proof_builder.h"
 #include "library/tactic/proof_state.h"
diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp
index 12ffdc33b..c0f7e8a8b 100644
--- a/src/library/tactic/proof_state.cpp
+++ b/src/library/tactic/proof_state.cpp
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "util/sstream.h"
 #include "kernel/builtin.h"
 #include "kernel/type_checker.h"
+#include "library/io_state_stream.h"
 #include "library/kernel_bindings.h"
 #include "library/tactic/proof_state.h"
 
diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp
index 440fc95c2..5610bdf7f 100644
--- a/src/library/tactic/tactic.cpp
+++ b/src/library/tactic/tactic.cpp
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "util/sstream.h"
 #include "util/interrupt.h"
 #include "util/lazy_list_fn.h"
+#include "library/io_state_stream.h"
 #include "kernel/replace_visitor.h"
 #include "kernel/instantiate.h"
 #include "kernel/update_expr.h"
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index ba101050b..8f5730c90 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -22,6 +22,7 @@ Author: Leonardo de Moura
 #include "kernel/formatter.h"
 #include "kernel/io_state.h"
 #include "library/kernel_bindings.h"
+#include "library/io_state_stream.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/shell.h"
 #include "frontends/lean/frontend.h"
diff --git a/src/tests/frontends/lean/frontend.cpp b/src/tests/frontends/lean/frontend.cpp
index 1f2a20a0f..bab9443fd 100644
--- a/src/tests/frontends/lean/frontend.cpp
+++ b/src/tests/frontends/lean/frontend.cpp
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/printer.h"
 #include "library/bin_op.h"
+#include "library/io_state_stream.h"
 #include "frontends/lean/frontend.h"
 #include "frontends/lean/operator_info.h"
 #include "frontends/lean/pp.h"
diff --git a/src/tests/frontends/lean/parser.cpp b/src/tests/frontends/lean/parser.cpp
index f1737d83c..de7b7dd1c 100644
--- a/src/tests/frontends/lean/parser.cpp
+++ b/src/tests/frontends/lean/parser.cpp
@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "util/numerics/mpq.h"
 #include "kernel/builtin.h"
 #include "kernel/printer.h"
+#include "library/io_state_stream.h"
 #include "library/arith/arith.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/frontend.h"
diff --git a/src/tests/frontends/lean/pp.cpp b/src/tests/frontends/lean/pp.cpp
index 5f6cda659..14c72b16c 100644
--- a/src/tests/frontends/lean/pp.cpp
+++ b/src/tests/frontends/lean/pp.cpp
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/builtin.h"
 #include "kernel/printer.h"
+#include "library/io_state_stream.h"
 #include "frontends/lean/frontend.h"
 #include "frontends/lean/pp.h"
 using namespace lean;
diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp
index db0337126..ffe8552c8 100644
--- a/src/tests/kernel/environment.cpp
+++ b/src/tests/kernel/environment.cpp
@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "kernel/normalizer.h"
 #include "kernel/abstract.h"
 #include "kernel/printer.h"
+#include "library/io_state_stream.h"
 #include "library/arith/arith.h"
 #include "frontends/lean/frontend.h"
 using namespace lean;
diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp
index 16e10f08b..91c334c1a 100644
--- a/src/tests/kernel/metavar.cpp
+++ b/src/tests/kernel/metavar.cpp
@@ -20,6 +20,7 @@ Author: Leonardo de Moura
 #include "kernel/kernel_exception.h"
 #include "kernel/builtin.h"
 #include "kernel/io_state.h"
+#include "library/io_state_stream.h"
 #include "library/placeholder.h"
 #include "library/arith/arith.h"
 #include "frontends/lean/frontend.h"
diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp
index e77e1227c..188755a01 100644
--- a/src/tests/kernel/normalizer.cpp
+++ b/src/tests/kernel/normalizer.cpp
@@ -18,6 +18,7 @@ Author: Leonardo de Moura
 #include "kernel/printer.h"
 #include "kernel/metavar.h"
 #include "kernel/free_vars.h"
+#include "library/io_state_stream.h"
 #include "library/deep_copy.h"
 #include "library/arith/int.h"
 #include "frontends/lean/frontend.h"
diff --git a/src/tests/kernel/threads.cpp b/src/tests/kernel/threads.cpp
index fc41de9be..749f819c3 100644
--- a/src/tests/kernel/threads.cpp
+++ b/src/tests/kernel/threads.cpp
@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "kernel/free_vars.h"
 #include "kernel/abstract.h"
 #include "kernel/normalizer.h"
+#include "library/io_state_stream.h"
 #include "library/max_sharing.h"
 #include "library/deep_copy.h"
 #include "library/arith/arith.h"
diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp
index 158619b33..88fead707 100644
--- a/src/tests/kernel/type_checker.cpp
+++ b/src/tests/kernel/type_checker.cpp
@@ -21,6 +21,7 @@ Author: Leonardo de Moura
 #include "kernel/kernel_exception.h"
 #include "kernel/type_checker_justification.h"
 #include "kernel/io_state.h"
+#include "library/io_state_stream.h"
 #include "library/arith/arith.h"
 #include "frontends/lean/frontend.h"
 using namespace lean;
diff --git a/src/tests/library/arith.cpp b/src/tests/library/arith.cpp
index 85e42e87d..df6e2b9cc 100644
--- a/src/tests/library/arith.cpp
+++ b/src/tests/library/arith.cpp
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/normalizer.h"
 #include "kernel/type_checker.h"
 #include "kernel/abstract.h"
+#include "library/io_state_stream.h"
 #include "library/arith/arith.h"
 #include "frontends/lean/frontend.h"
 using namespace lean;
diff --git a/src/tests/library/elaborator/elaborator.cpp b/src/tests/library/elaborator/elaborator.cpp
index 0a5b52d5f..4ca6365c9 100644
--- a/src/tests/library/elaborator/elaborator.cpp
+++ b/src/tests/library/elaborator/elaborator.cpp
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "kernel/normalizer.h"
 #include "kernel/instantiate.h"
 #include "kernel/builtin.h"
+#include "library/io_state_stream.h"
 #include "library/placeholder.h"
 #include "library/arith/arith.h"
 #include "library/elaborator/elaborator.h"
diff --git a/src/tests/library/rewriter/rewriter.cpp b/src/tests/library/rewriter/rewriter.cpp
index 642e6a187..6317e45c4 100644
--- a/src/tests/library/rewriter/rewriter.cpp
+++ b/src/tests/library/rewriter/rewriter.cpp
@@ -12,6 +12,7 @@ Author: Soonho Kong
 #include "kernel/printer.h"
 #include "kernel/io_state.h"
 #include "kernel/builtin.h"
+#include "library/io_state_stream.h"
 #include "library/arith/arith.h"
 #include "library/arith/nat.h"
 #include "library/rewriter/fo_match.h"
diff --git a/src/tests/library/tactic/tactic.cpp b/src/tests/library/tactic/tactic.cpp
index 75379a8db..caef5707f 100644
--- a/src/tests/library/tactic/tactic.cpp
+++ b/src/tests/library/tactic/tactic.cpp
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "util/interrupt.h"
 #include "kernel/builtin.h"
 #include "kernel/kernel_exception.h"
+#include "library/io_state_stream.h"
 #include "library/tactic/goal.h"
 #include "library/tactic/proof_builder.h"
 #include "library/tactic/proof_state.h"