diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt
index 750b8024b..d7b922e6c 100644
--- a/src/library/tactic/CMakeLists.txt
+++ b/src/library/tactic/CMakeLists.txt
@@ -1,4 +1,5 @@
-add_library(tactic goal.cpp proof_state.cpp tactic.cpp apply_tactic.cpp
-intros_tactic.cpp rename_tactic.cpp expr_to_tactic.cpp init_module.cpp)
+add_library(tactic goal.cpp proof_state.cpp tactic.cpp
+apply_tactic.cpp intros_tactic.cpp rename_tactic.cpp trace_tactic.cpp
+expr_to_tactic.cpp init_module.cpp)
 
 target_link_libraries(tactic ${LEAN_LIBS})
diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp
index 2aa2c69d8..3372b56df 100644
--- a/src/library/tactic/expr_to_tactic.cpp
+++ b/src/library/tactic/expr_to_tactic.cpp
@@ -342,26 +342,6 @@ void initialize_expr_to_tactic() {
                      [](tactic const & t1, tactic const & t2) { return orelse(t1, t2); });
     register_unary_tac(repeat_tac_name,
                        [](tactic const & t1) { return repeat(t1); });
-    register_tac(name(*g_tactic_name, "state"),
-                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const * p) {
-                     if (p)
-                         if (auto it = p->get_pos_info(e))
-                             return trace_state_tactic(std::string(p->get_file_name()), *it);
-                     return trace_state_tactic();
-                 });
-    register_tac(name(*g_tactic_name, "trace"),
-                 [](type_checker & tc, elaborate_fn const &, expr const & e, pos_info_provider const *) {
-                     buffer<expr> args;
-                     get_app_args(e, args);
-                     if (args.size() != 1)
-                         throw expr_to_tactic_exception(e, "invalid trace tactic, argument expected");
-                     if (auto str = to_string(args[0]))
-                         return trace_tactic(*str);
-                     else if (auto str = to_string(tc.whnf(args[0]).first))
-                         return trace_tactic(*str);
-                     else
-                         throw expr_to_tactic_exception(e, "invalid trace tactic, string value expected");
-                 });
     register_tac(exact_tac_name,
                  [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
                      // TODO(Leo): use elaborate_fn
diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp
index dec2b2814..d899e41ca 100644
--- a/src/library/tactic/init_module.cpp
+++ b/src/library/tactic/init_module.cpp
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "library/tactic/apply_tactic.h"
 #include "library/tactic/rename_tactic.h"
 #include "library/tactic/intros_tactic.h"
+#include "library/tactic/trace_tactic.h"
 
 namespace lean {
 void initialize_tactic_module() {
@@ -17,9 +18,11 @@ void initialize_tactic_module() {
     initialize_apply_tactic();
     initialize_rename_tactic();
     initialize_intros_tactic();
+    initialize_trace_tactic();
 }
 
 void finalize_tactic_module() {
+    finalize_trace_tactic();
     finalize_intros_tactic();
     finalize_rename_tactic();
     finalize_apply_tactic();
diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp
index 7665a3791..226ef8b4b 100644
--- a/src/library/tactic/tactic.cpp
+++ b/src/library/tactic/tactic.cpp
@@ -88,48 +88,6 @@ tactic cond(proof_state_pred p, tactic const & t1, tactic const & t2) {
         });
 }
 
-tactic trace_tactic(std::string const & msg) {
-    return tactic1([=](environment const &, io_state const & ios, proof_state const & s) -> proof_state {
-            ios.get_diagnostic_channel() << msg << "\n";
-            ios.get_diagnostic_channel().get_stream().flush();
-            return s;
-        });
-}
-
-tactic trace_tactic(sstream const & msg) {
-    return trace_tactic(msg.str());
-}
-
-tactic trace_tactic(char const * msg) {
-    return trace_tactic(std::string(msg));
-}
-
-tactic trace_state_tactic(std::string const & fname, pair<unsigned, unsigned> const & pos) {
-    return tactic1([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state {
-            diagnostic(env, ios) << fname << ":" << pos.first << ":" << pos.second << ": proof state\n"
-                                 << s << endl;
-            ios.get_diagnostic_channel().get_stream().flush();
-            return s;
-        });
-}
-
-tactic trace_state_tactic() {
-    return tactic1([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state {
-            diagnostic(env, ios) << "proof state\n" << s << endl;
-            ios.get_diagnostic_channel().get_stream().flush();
-            return s;
-        });
-}
-
-tactic suppress_trace(tactic const & t) {
-    return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
-            io_state new_ios(ios);
-            std::shared_ptr<output_channel> out(std::make_shared<string_output_channel>());
-            new_ios.set_diagnostic_channel(out);
-            return t(env, new_ios, s);
-        });
-}
-
 tactic then(tactic const & t1, tactic const & t2) {
     return tactic([=](environment const & env, io_state const & ios, proof_state const & s1) -> proof_state_seq {
             return map_append(t1(env, ios, s1), [=](proof_state const & s2) {
@@ -473,7 +431,6 @@ static int tactic_par(lua_State * L)            {  return push_tactic(L, par(to_
 static int tactic_repeat(lua_State * L)         {  return push_tactic(L, repeat(to_tactic(L, 1))); }
 static int tactic_repeat_at_most(lua_State * L) {  return push_tactic(L, repeat_at_most(to_tactic(L, 1), luaL_checkinteger(L, 2))); }
 static int tactic_take(lua_State * L)           {  return push_tactic(L, take(to_tactic(L, 1), luaL_checkinteger(L, 2))); }
-static int tactic_suppress_trace(lua_State * L) {  return push_tactic(L, suppress_trace(to_tactic(L, 1))); }
 static int tactic_try_for(lua_State * L)        {  return push_tactic(L, try_for(to_tactic(L, 1), luaL_checkinteger(L, 2))); }
 static int tactic_using_params(lua_State * L)   {  return push_tactic(L, using_params(to_tactic(L, 1), to_options(L, 2))); }
 static int tactic_focus(lua_State * L) {
@@ -528,7 +485,6 @@ static int mk_lua_when_tactic(lua_State * L) { return mk_lua_cond_tactic(L, to_t
 static int mk_id_tactic(lua_State * L)          {  return push_tactic(L, id_tactic()); }
 static int mk_now_tactic(lua_State * L)         {  return push_tactic(L, now_tactic()); }
 static int mk_fail_tactic(lua_State * L)        {  return push_tactic(L, fail_tactic()); }
-static int mk_trace_tactic(lua_State * L)       {  return push_tactic(L, trace_tactic(luaL_checkstring(L, 1))); }
 static int mk_assumption_tactic(lua_State * L)  {  return push_tactic(L, assumption_tactic()); }
 static int mk_unfold_tactic(lua_State * L)      {
     int nargs = lua_gettop(L);
@@ -552,7 +508,6 @@ static const struct luaL_Reg tactic_m[] = {
     {"repeat",          safe_function<tactic_repeat>},
     {"repeat_at_most",  safe_function<tactic_repeat_at_most>},
     {"take",            safe_function<tactic_take>},
-    {"suppress_trace",  safe_function<tactic_suppress_trace>},
     {"try_for",         safe_function<tactic_try_for>},
     {"using_params",    safe_function<tactic_using_params>},
     {"using",           safe_function<tactic_using_params>},
@@ -573,7 +528,6 @@ void open_tactic(lua_State * L) {
     setfuncs(L, tactic_m, 0);
 
     SET_GLOBAL_FUN(tactic_pred,           "is_tactic");
-    SET_GLOBAL_FUN(mk_trace_tactic,       "trace_tac");
     SET_GLOBAL_FUN(mk_id_tactic,          "id_tac");
     SET_GLOBAL_FUN(mk_now_tactic,         "now_tac");
     SET_GLOBAL_FUN(mk_fail_tactic,        "fail_tac");
diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h
index c45297e07..0e3d2f39b 100644
--- a/src/library/tactic/tactic.h
+++ b/src/library/tactic/tactic.h
@@ -51,16 +51,6 @@ tactic fail_tactic();
 tactic now_tactic();
 /** \brief Return a tactic that solves any goal of the form  <tt>..., H : A, ... |- A</tt>. */
 tactic assumption_tactic();
-/** \brief Return a tactic that just returns the input state, and display the given message in the diagnostic channel. */
-tactic trace_tactic(char const * msg);
-class sstream;
-tactic trace_tactic(sstream const & msg);
-tactic trace_tactic(std::string const & msg);
-/** \brief Return a tactic that just displays the input state in the diagnostic channel. */
-tactic trace_state_tactic(std::string const & fname, pair<unsigned, unsigned> const & pos);
-tactic trace_state_tactic();
-/** \brief Create a tactic that applies \c t, but suppressing diagnostic messages. */
-tactic suppress_trace(tactic const & t);
 /** \brief Return a tactic that performs \c t1 followed by \c t2. */
 tactic then(tactic const & t1, tactic const & t2);
 inline tactic operator<<(tactic const & t1, tactic const & t2) { return then(t1, t2); }
diff --git a/src/library/tactic/trace_tactic.cpp b/src/library/tactic/trace_tactic.cpp
new file mode 100644
index 000000000..8fe79cec3
--- /dev/null
+++ b/src/library/tactic/trace_tactic.cpp
@@ -0,0 +1,84 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <string>
+#include "util/sstream.h"
+#include "kernel/type_checker.h"
+#include "library/string.h"
+#include "library/tactic/tactic.h"
+#include "library/tactic/expr_to_tactic.h"
+
+namespace lean {
+
+tactic trace_tactic(std::string const & msg) {
+    return tactic1([=](environment const &, io_state const & ios, proof_state const & s) -> proof_state {
+            ios.get_diagnostic_channel() << msg << "\n";
+            ios.get_diagnostic_channel().get_stream().flush();
+            return s;
+        });
+}
+
+tactic trace_tactic(sstream const & msg) {
+    return trace_tactic(msg.str());
+}
+
+tactic trace_tactic(char const * msg) {
+    return trace_tactic(std::string(msg));
+}
+
+tactic trace_state_tactic(std::string const & fname, pair<unsigned, unsigned> const & pos) {
+    return tactic1([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state {
+            diagnostic(env, ios) << fname << ":" << pos.first << ":" << pos.second << ": proof state\n"
+                                 << s << endl;
+            ios.get_diagnostic_channel().get_stream().flush();
+            return s;
+        });
+}
+
+tactic trace_state_tactic() {
+    return tactic1([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state {
+            diagnostic(env, ios) << "proof state\n" << s << endl;
+            ios.get_diagnostic_channel().get_stream().flush();
+            return s;
+        });
+}
+
+tactic suppress_trace(tactic const & t) {
+    return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
+            io_state new_ios(ios);
+            std::shared_ptr<output_channel> out(std::make_shared<string_output_channel>());
+            new_ios.set_diagnostic_channel(out);
+            return t(env, new_ios, s);
+        });
+}
+
+void initialize_trace_tactic() {
+    register_tac(name({"tactic", "state"}),
+                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const * p) {
+                     if (p)
+                         if (auto it = p->get_pos_info(e))
+                             return trace_state_tactic(std::string(p->get_file_name()), *it);
+                     return trace_state_tactic();
+                 });
+
+    register_tac(name({"tactic", "trace"}),
+                 [](type_checker & tc, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+                     buffer<expr> args;
+                     get_app_args(e, args);
+                     if (args.size() != 1)
+                         throw expr_to_tactic_exception(e, "invalid trace tactic, argument expected");
+                     if (auto str = to_string(args[0]))
+                         return trace_tactic(*str);
+                     else if (auto str = to_string(tc.whnf(args[0]).first))
+                         return trace_tactic(*str);
+                     else
+                         throw expr_to_tactic_exception(e, "invalid trace tactic, string value expected");
+                 });
+}
+
+void finalize_trace_tactic() {
+}
+}
diff --git a/src/library/tactic/trace_tactic.h b/src/library/tactic/trace_tactic.h
new file mode 100644
index 000000000..efd56ef52
--- /dev/null
+++ b/src/library/tactic/trace_tactic.h
@@ -0,0 +1,25 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <string>
+#include "library/tactic/tactic.h"
+
+namespace lean {
+/** \brief Return a tactic that just returns the input state, and display the given message in the diagnostic channel. */
+tactic trace_tactic(char const * msg);
+class sstream;
+tactic trace_tactic(sstream const & msg);
+tactic trace_tactic(std::string const & msg);
+/** \brief Return a tactic that just displays the input state in the diagnostic channel. */
+tactic trace_state_tactic(std::string const & fname, pair<unsigned, unsigned> const & pos);
+tactic trace_state_tactic();
+/** \brief Create a tactic that applies \c t, but suppressing diagnostic messages. */
+tactic suppress_trace(tactic const & t);
+
+void initialize_trace_tactic();
+void finalize_trace_tactic();
+}
diff --git a/tests/lua/old/tactic1.lua b/tests/lua/old/tactic1.lua
index bc91677b3..b7de41b3a 100644
--- a/tests/lua/old/tactic1.lua
+++ b/tests/lua/old/tactic1.lua
@@ -15,24 +15,3 @@ local ltac = tactic(function(env, ios, s)
                        print("FIRST tactic in Lua, current state: " .. tostring(s));
                        return s
 end)
-local t = (trace_tac("hello") .. trace_tac("world")) + (trace_tac("again") .. ltac .. assumption_tac())
-for s in t(env, ios, ps) do
-   if s:is_proof_final_state() then
-      local m = proof_map()
-      local a = assignment(s:get_menv())
-      print(s:proof_builder()(m, a))
-   else
-      print(s)
-   end
-end
-print("-------------------")
-print(t:solve(env, ios, ps))
-print(t:solve(env, ios, ctx, p))
-assert(t:solve(env, ios, ps) == Var(1))
-assert(t:solve(env, ios, ctx, q) == Var(0))
-local t2 = id_tac() + id_tac() + id_tac()
-local r  = t2:solve(env, ios, ps)
-assert(#r == 3)
-for i, out_state in ipairs(r) do
-   print(i, out_state)
-end
diff --git a/tests/lua/tactic1.lua b/tests/lua/tactic1.lua
index a20e38eca..b20284203 100644
--- a/tests/lua/tactic1.lua
+++ b/tests/lua/tactic1.lua
@@ -7,9 +7,7 @@ local b  = Local("b", A)
 local H  = Local("H", eq(A, a, b))
 local m  = mk_metavar("m", Pi(A, a, b, H, eq(A, a, b)))(A, a, b, H)
 local s  = to_proof_state(m, eq(A, a, b))
-local t = Then(Append(trace_tac("tst1a"), trace_tac("tst1b")),
-               trace_tac("tst2"),
-               Append(trace_tac("tst3"), assumption_tac()))
+local t = assumption_tac()
 for r in t(env, s) do
    print("Solution:")
    print(r)