diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index f8fd08084..432a2d6f8 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "kernel/abstract.h"
 #include "kernel/io_state.h"
+#include "kernel/decl_macros.h"
 
 namespace lean {
 // =======================================
diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h
index 8410315c4..bba2b4299 100644
--- a/src/kernel/builtin.h
+++ b/src/kernel/builtin.h
@@ -219,33 +219,5 @@ inline expr ExistsElim(expr const & A, expr const & P, expr const & B, expr cons
 expr mk_exists_intro_fn();
 inline expr ExistsIntro(expr const & A, expr const & P, expr const & a, expr const & H) { return mk_app(mk_exists_intro_fn(), A, P, a, H); }
 
-/**
-   \brief Helper macro for defining constants such as bool_type, int_type, int_add, etc.
-*/
-#define MK_BUILTIN(Name, ClassName)                                     \
-expr mk_##Name() {                                                      \
-    static LEAN_THREAD_LOCAL expr r = mk_value(*(new ClassName()));     \
-    return r;                                                           \
-}
-
-/**
-   \brief Helper macro for generating "defined" constants.
-*/
-#define MK_CONSTANT(Name, NameObj)                                      \
-static name Name ## _name = NameObj;                                    \
-expr mk_##Name() {                                                      \
-    static LEAN_THREAD_LOCAL expr r = mk_constant(Name ## _name);       \
-    return r ;                                                          \
-}                                                                       \
-bool is_ ## Name(expr const & e) {                                      \
-    return is_constant(e) && const_name(e) == Name ## _name;            \
-}
-
-#define MK_IS_BUILTIN(Name, Builtin)                                    \
-bool Name(expr const & e) {                                             \
-    expr const & v = Builtin;                                           \
-    return e == v || (is_constant(e) && const_name(e) == to_value(v).get_name()); \
-}
-
 void import_kernel(environment const & env);
 }
diff --git a/src/kernel/decl_macros.h b/src/kernel/decl_macros.h
new file mode 100644
index 000000000..21eec3861
--- /dev/null
+++ b/src/kernel/decl_macros.h
@@ -0,0 +1,34 @@
+/*
+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
+/**
+   \brief Helper macro for defining constants such as bool_type, int_type, int_add, etc.
+*/
+#define MK_BUILTIN(Name, ClassName)                                     \
+expr mk_##Name() {                                                      \
+    static LEAN_THREAD_LOCAL expr r = mk_value(*(new ClassName()));     \
+    return r;                                                           \
+}
+
+/**
+   \brief Helper macro for generating "defined" constants.
+*/
+#define MK_CONSTANT(Name, NameObj)                                      \
+static name Name ## _name = NameObj;                                    \
+expr mk_##Name() {                                                      \
+    static LEAN_THREAD_LOCAL expr r = mk_constant(Name ## _name);       \
+    return r ;                                                          \
+}                                                                       \
+bool is_ ## Name(expr const & e) {                                      \
+    return is_constant(e) && const_name(e) == Name ## _name;            \
+}
+
+#define MK_IS_BUILTIN(Name, Builtin)                                    \
+bool Name(expr const & e) {                                             \
+    expr const & v = Builtin;                                           \
+    return e == v || (is_constant(e) && const_name(e) == to_value(v).get_name()); \
+}
diff --git a/src/library/arith/int.cpp b/src/library/arith/int.cpp
index 245803c17..4d3d0c6f9 100644
--- a/src/library/arith/int.cpp
+++ b/src/library/arith/int.cpp
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "kernel/value.h"
 #include "kernel/io_state.h"
+#include "kernel/decl_macros.h"
 #include "library/kernel_bindings.h"
 #include "library/arith/int.h"
 #include "library/arith/nat.h"
diff --git a/src/library/arith/nat.cpp b/src/library/arith/nat.cpp
index d449fb2e3..933ac9b98 100644
--- a/src/library/arith/nat.cpp
+++ b/src/library/arith/nat.cpp
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "kernel/value.h"
 #include "kernel/io_state.h"
+#include "kernel/decl_macros.h"
 #include "library/kernel_bindings.h"
 #include "library/arith/nat.h"
 
diff --git a/src/library/arith/real.cpp b/src/library/arith/real.cpp
index a1d7f3486..d8fea49ee 100644
--- a/src/library/arith/real.cpp
+++ b/src/library/arith/real.cpp
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "kernel/value.h"
 #include "kernel/io_state.h"
+#include "kernel/decl_macros.h"
 #include "library/kernel_bindings.h"
 #include "library/arith/real.h"
 #include "library/arith/int.h"