diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index 0bf0c201c..0c6410fc2 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include <getopt.h>
 #include <string>
 #include "util/stackinfo.h"
+#include "util/macros.h"
 #include "util/debug.h"
 #include "util/sstream.h"
 #include "util/interrupt.h"
@@ -60,13 +61,10 @@ static void on_ctrl_c(int ) {
     lean::request_interrupt();
 }
 
-#define XSTR(x) #x
-#define STR(x) XSTR(x)
-
 static void display_header(std::ostream & out) {
     out << "Lean (version " << LEAN_VERSION_MAJOR << "." << LEAN_VERSION_MINOR
         << ", commit " << std::string(g_githash).substr(0, 12)
-        << ", " << STR(LEAN_BUILD_TYPE) << ")\n";
+        << ", " << LEAN_STR(LEAN_BUILD_TYPE) << ")\n";
 }
 
 static void display_help(std::ostream & out) {
diff --git a/src/util/macros.h b/src/util/macros.h
new file mode 100644
index 000000000..bc1193ead
--- /dev/null
+++ b/src/util/macros.h
@@ -0,0 +1,10 @@
+/*
+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
+
+#define LEAN_XSTR(x) #x
+#define LEAN_STR(x) LEAN_XSTR(x)
diff --git a/src/util/sexpr/option_declarations.h b/src/util/sexpr/option_declarations.h
index 81fbaa255..1c2367c63 100644
--- a/src/util/sexpr/option_declarations.h
+++ b/src/util/sexpr/option_declarations.h
@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <map>
 #include <string>
+#include "util/macros.h"
 #include "util/sexpr/options.h"
 
 namespace lean {
@@ -36,6 +37,6 @@ void initialize_option_declarations();
 void finalize_option_declarations();
 option_declarations const & get_option_declarations();
 void register_option(name const & n, option_kind k, char const * default_value, char const * description);
-#define register_bool_option(n, v, d) register_option(n, BoolOption, #v, d)
-#define register_unsigned_option(n, v, d) register_option(n, UnsignedOption, #v, d)
+#define register_bool_option(n, v, d) register_option(n, BoolOption, LEAN_STR(v), d)
+#define register_unsigned_option(n, v, d) register_option(n, UnsignedOption, LEAN_STR(v), d)
 }
diff --git a/src/util/sexpr/options.h b/src/util/sexpr/options.h
index 378726da9..70464b95d 100644
--- a/src/util/sexpr/options.h
+++ b/src/util/sexpr/options.h
@@ -90,14 +90,6 @@ struct mk_option_declaration {
 
 int mk_options(name const & prefix, lua_State * L);
 
-#define LEAN_MAKE_OPTION_NAME_CORE(LINE) LEAN_OPTION_ ## LINE
-#define LEAN_MAKE_OPTION_NAME(LINE) LEAN_MAKE_OPTION_NAME_CORE(LINE)
-#define LEAN_OPTION_UNIQUE_NAME LEAN_MAKE_OPTION_NAME(__LINE__)
-#define RegisterOption(N, K, D, DESC) static ::lean::mk_option_declaration LEAN_OPTION_UNIQUE_NAME(N, K, D, DESC)
-#define RegisterOptionCore(N, K, D, DESC) RegisterOption(N, K, #D, DESC)
-#define RegisterBoolOption(N, D, DESC) RegisterOptionCore(N, BoolOption, D, DESC);
-#define RegisterUnsignedOption(N, D, DESC) RegisterOptionCore(N, UnsignedOption, D, DESC);
-
 UDATA_DEFS(options)
 int options_update(lua_State * L);
 /**