diff --git a/src/initialize/init.cpp b/src/initialize/init.cpp
index 50c2ddb439..a9362e0c57 100644
--- a/src/initialize/init.cpp
+++ b/src/initialize/init.cpp
@@ -17,8 +17,8 @@ Author: Leonardo de Moura
 #include "initialize/init.h"
 
 namespace lean {
-extern "C" object* initialize_Init(object* w);
-extern "C" object* initialize_Lean(object* w);
+extern "C" object* initialize_Init(uint8_t, object* w);
+extern "C" object* initialize_Lean(uint8_t, object* w);
 
 /* Initializes the Lean runtime. Before executing any code which uses the Lean package,
 you must first call this function, and then `lean::io_mark_end_initialization`. Inbetween
@@ -26,8 +26,9 @@ these two calls, you may also have to run additional initializers for your own m
 extern "C" LEAN_EXPORT void lean_initialize() {
     save_stack_info();
     initialize_util_module();
-    consume_io_result(initialize_Init(io_mk_world()));
-    consume_io_result(initialize_Lean(io_mk_world()));
+    uint8_t builtin = 1;
+    consume_io_result(initialize_Init(builtin, io_mk_world()));
+    consume_io_result(initialize_Lean(builtin, io_mk_world()));
     initialize_kernel_module();
     init_default_print_fn();
     initialize_library_core_module();
diff --git a/src/util/shell.cpp b/src/util/shell.cpp
index 39c1c84abf..9a24466ae5 100644
--- a/src/util/shell.cpp
+++ b/src/util/shell.cpp
@@ -334,8 +334,8 @@ void load_plugin(std::string path) {
     if (!init) {
         throw exception(sstream() << "error, plugin " << path << " does not seem to contain a module '" << pkg << "'");
     }
-    auto init_fn = reinterpret_cast<object *(*)(object *)>(init);
-    object *r = init_fn(io_mk_world());
+    auto init_fn = reinterpret_cast<object *(*)(uint8_t, object *)>(init);
+    object *r = init_fn(1 /* builtin */, io_mk_world());
     consume_io_result(r);
     // NOTE: we never unload plugins
 }