diff --git a/src/bindings/lua/expr.cpp b/src/bindings/lua/expr.cpp
index a4bfe73e1a..ad275deb56 100644
--- a/src/bindings/lua/expr.cpp
+++ b/src/bindings/lua/expr.cpp
@@ -172,18 +172,6 @@ void open_expr(lua_State * L) {
     lua_setfield(L, -2, "__index");
     setfuncs(L, expr_m, 0);
 
-    dostring(L, R"Lua(
-function Consts(s)
-   r = {}
-   i = 1
-   for c in string.gmatch(s, '[^ ,;\t\n]+') do
-      r[i] = Const(c)
-      i = i + 1
-   end
-   return unpack(r)
-end
-)Lua");
-
     set_global_function<expr_mk_constant>(L, "mk_constant");
     set_global_function<expr_mk_constant>(L, "Const");
     set_global_function<expr_mk_var>(L, "mk_var");
diff --git a/src/bindings/lua/lean.lua b/src/bindings/lua/lean.lua
new file mode 100644
index 0000000000..ba38736e8a
--- /dev/null
+++ b/src/bindings/lua/lean.lua
@@ -0,0 +1,11 @@
+static char const * g_leanlua_extra = R"Lua(
+function Consts(s)
+  r = {}
+  i = 1
+  for c in string.gmatch(s, '[^ ,;\t\n]+') do
+     r[i] = Const(c)
+     i = i + 1
+  end
+  return unpack(r)
+end
+)Lua";
diff --git a/src/bindings/lua/leanlua_state.cpp b/src/bindings/lua/leanlua_state.cpp
index c2a6c8d3a6..da162c9344 100644
--- a/src/bindings/lua/leanlua_state.cpp
+++ b/src/bindings/lua/leanlua_state.cpp
@@ -19,6 +19,7 @@ Author: Leonardo de Moura
 #include "bindings/lua/sexpr.h"
 #include "bindings/lua/format.h"
 #include "bindings/lua/expr.h"
+#include "bindings/lua/lean.lua"
 
 extern "C" void * lua_realloc(void *, void * q, size_t, size_t new_size) { return lean::realloc(q, new_size); }
 
@@ -43,6 +44,7 @@ struct leanlua_state::imp {
         lean::open_sexpr(m_state);
         lean::open_format(m_state);
         lean::open_expr(m_state);
+        dostring(g_leanlua_extra);
     }
 
     ~imp() {