diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index badcddfd6..21de2b9a7 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "util/script_state.h"
 #include "util/list_lua.h"
 #include "util/pair_lua.h"
+#include "util/lua_named_param.h"
 #include "util/luaref.h"
 #include "kernel/abstract.h"
 #include "kernel/for_each_fn.h"
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 8cbbd2aa8..7dfc3d182 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -4,10 +4,11 @@ else()
   set(THREAD_CPP "")
 endif()
 
-add_library(util trace.cpp debug.cpp name.cpp name_set.cpp name_generator.cpp
-  exception.cpp interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp
-  safe_arith.cpp ascii.cpp memory.cpp shared_mutex.cpp realpath.cpp
-  script_state.cpp script_exception.cpp rb_map.cpp lua.cpp
-  luaref.cpp stackinfo.cpp lean_path.cpp serializer.cpp lbool.cpp ${THREAD_CPP})
+add_library(util trace.cpp debug.cpp name.cpp name_set.cpp
+  name_generator.cpp exception.cpp interrupt.cpp hash.cpp escaped.cpp
+  bit_tricks.cpp safe_arith.cpp ascii.cpp memory.cpp shared_mutex.cpp
+  realpath.cpp script_state.cpp script_exception.cpp rb_map.cpp
+  lua.cpp luaref.cpp lua_named_param.cpp stackinfo.cpp lean_path.cpp
+  serializer.cpp lbool.cpp ${THREAD_CPP})
 
 target_link_libraries(util ${LEAN_LIBS})
diff --git a/src/util/lua.cpp b/src/util/lua.cpp
index b46d844b1..30da54929 100644
--- a/src/util/lua.cpp
+++ b/src/util/lua.cpp
@@ -195,76 +195,5 @@ lua_migrate_fn get_migrate_fn(lua_State * L, int i) {
     }
     return nullptr;
 }
-
-bool get_bool_named_param(lua_State * L, int idx, char const * opt_name, bool def_value) {
-    if (lua_istable(L, idx)) {
-        bool result = def_value;
-        push_string(L, opt_name);
-        lua_gettable(L, idx);
-        if (lua_isboolean(L, -1)) {
-            result = lua_toboolean(L, -1);
-            lua_pop(L, 1);
-            return result;
-        } else if (lua_isnil(L, -1)) {
-            lua_pop(L, 1);
-            return result;
-        } else {
-            lua_pop(L, 1);
-            throw exception(sstream() << "field '" << opt_name << "' must be a Boolean in table at arg #" << idx);
-        }
-    } else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) {
-        throw exception(sstream() << "arg #" << idx << " must be a table");
-    } else {
-        return def_value;
-    }
-}
-
-int get_int_named_param(lua_State * L, int idx, char const * opt_name, int def_value) {
-    if (lua_istable(L, idx)) {
-        int result = def_value;
-        push_string(L, opt_name);
-        lua_gettable(L, idx);
-        if (lua_isnumber(L, -1)) {
-            result = lua_tointeger(L, -1);
-            lua_pop(L, 1);
-            return result;
-        } else if (lua_isnil(L, -1)) {
-            lua_pop(L, 1);
-            return result;
-        } else {
-            lua_pop(L, 1);
-            throw exception(sstream() << "field '" << opt_name << "' must be an integer in table at arg #" << idx);
-        }
-    } else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) {
-        throw exception(sstream() << "arg #" << idx << " must be a table");
-    } else {
-        return def_value;
-    }
-}
-
-unsigned get_uint_named_param(lua_State * L, int idx, char const * opt_name, unsigned def_value) {
-    if (lua_istable(L, idx)) {
-        long result = def_value;
-        push_string(L, opt_name);
-        lua_gettable(L, idx);
-        if (lua_isnumber(L, -1)) {
-            long result = lua_tointeger(L, -1);
-            lua_pop(L, 1);
-            if (result < 0 || result > std::numeric_limits<unsigned>::max())
-                throw exception(sstream() << "field '" << opt_name << "' must be a unsigned integer in table at arg #" << idx);
-            return static_cast<unsigned>(result);
-        } else if (lua_isnil(L, -1)) {
-            lua_pop(L, 1);
-            return static_cast<unsigned>(result);
-        } else {
-            lua_pop(L, 1);
-            throw exception(sstream() << "field '" << opt_name << "' must be an integer in table at arg #" << idx);
-        }
-    } else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) {
-        throw exception(sstream() << "arg #" << idx << " must be a table");
-    } else {
-        return def_value;
-    }
-}
 }
 
diff --git a/src/util/lua.h b/src/util/lua.h
index fcc27cfcd..a97081956 100644
--- a/src/util/lua.h
+++ b/src/util/lua.h
@@ -1,5 +1,5 @@
 /*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
@@ -138,12 +138,4 @@ inline int push_integer(lua_State * L, lua_Integer v) { lua_pushinteger(L, v); r
 inline int push_number(lua_State * L, lua_Number v) { lua_pushnumber(L, v); return 1; }
 inline int push_nil(lua_State * L) { lua_pushnil(L); return 1; }
 // =======================================
-
-// =======================================
-// Utilities for simulating Python-like named parameters using Lua tables.
-// In the following function \c idx is the position of the Lua table on the Lua stack.
-bool get_bool_named_param(lua_State * L, int idx, char const * opt_name, bool def_value);
-int get_int_named_param(lua_State * L, int idx, char const * opt_name, int def_value);
-unsigned get_uint_named_param(lua_State * L, int idx, char const * opt_name, unsigned def_value);
-// =======================================
 }
diff --git a/src/util/lua_named_param.cpp b/src/util/lua_named_param.cpp
new file mode 100644
index 000000000..366645e77
--- /dev/null
+++ b/src/util/lua_named_param.cpp
@@ -0,0 +1,82 @@
+/*
+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 <limits>
+#include "util/lua_named_param.h"
+#include "util/sstream.h"
+
+namespace lean {
+bool get_bool_named_param(lua_State * L, int idx, char const * opt_name, bool def_value) {
+    if (lua_istable(L, idx)) {
+        bool result = def_value;
+        push_string(L, opt_name);
+        lua_gettable(L, idx);
+        if (lua_isboolean(L, -1)) {
+            result = lua_toboolean(L, -1);
+            lua_pop(L, 1);
+            return result;
+        } else if (lua_isnil(L, -1)) {
+            lua_pop(L, 1);
+            return result;
+        } else {
+            lua_pop(L, 1);
+            throw exception(sstream() << "field '" << opt_name << "' must be a Boolean in table at arg #" << idx);
+        }
+    } else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) {
+        throw exception(sstream() << "arg #" << idx << " must be a table");
+    } else {
+        return def_value;
+    }
+}
+
+int get_int_named_param(lua_State * L, int idx, char const * opt_name, int def_value) {
+    if (lua_istable(L, idx)) {
+        int result = def_value;
+        push_string(L, opt_name);
+        lua_gettable(L, idx);
+        if (lua_isnumber(L, -1)) {
+            result = lua_tointeger(L, -1);
+            lua_pop(L, 1);
+            return result;
+        } else if (lua_isnil(L, -1)) {
+            lua_pop(L, 1);
+            return result;
+        } else {
+            lua_pop(L, 1);
+            throw exception(sstream() << "field '" << opt_name << "' must be an integer in table at arg #" << idx);
+        }
+    } else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) {
+        throw exception(sstream() << "arg #" << idx << " must be a table");
+    } else {
+        return def_value;
+    }
+}
+
+unsigned get_uint_named_param(lua_State * L, int idx, char const * opt_name, unsigned def_value) {
+    if (lua_istable(L, idx)) {
+        push_string(L, opt_name);
+        lua_gettable(L, idx);
+        if (lua_isnumber(L, -1)) {
+            long result = lua_tointeger(L, -1);
+            lua_pop(L, 1);
+            if (result < 0 || result > std::numeric_limits<unsigned>::max())
+                throw exception(sstream() << "field '" << opt_name << "' must be a unsigned integer in table at arg #" << idx);
+            return static_cast<unsigned>(result);
+        } else if (lua_isnil(L, -1)) {
+            lua_pop(L, 1);
+            return static_cast<unsigned>(def_value);
+        } else {
+            lua_pop(L, 1);
+            throw exception(sstream() << "field '" << opt_name << "' must be an integer in table at arg #" << idx);
+        }
+    } else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) {
+        throw exception(sstream() << "arg #" << idx << " must be a table");
+    } else {
+        return def_value;
+    }
+}
+}
+
diff --git a/src/util/lua_named_param.h b/src/util/lua_named_param.h
new file mode 100644
index 000000000..06799facf
--- /dev/null
+++ b/src/util/lua_named_param.h
@@ -0,0 +1,18 @@
+/*
+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 "util/lua.h"
+#include "util/optional.h"
+
+namespace lean {
+// =======================================
+// Utilities for simulating Python-like named parameters using Lua tables.
+// In the following function \c idx is the position of the Lua table on the Lua stack.
+bool get_bool_named_param(lua_State * L, int idx, char const * opt_name, bool def_value);
+int get_int_named_param(lua_State * L, int idx, char const * opt_name, int def_value);
+unsigned get_uint_named_param(lua_State * L, int idx, char const * opt_name, unsigned def_value);
+}