diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 176128d118..70933775c1 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -341,6 +341,8 @@ add_subdirectory(library/constructions)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:constructions>)
 add_subdirectory(library/equations_compiler)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:equations_compiler>)
+add_subdirectory(library/inductive_compiler)
+set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:inductive_compiler>)
 # add_subdirectory(library/blast)
 # set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:blast>)
 # add_subdirectory(library/blast/backward)
diff --git a/src/init/init.cpp b/src/init/init.cpp
index 5cb774e079..affeb2e67d 100644
--- a/src/init/init.cpp
+++ b/src/init/init.cpp
@@ -17,6 +17,7 @@ Author: Leonardo de Moura
 #include "library/tactic/init_module.h"
 #include "library/constructions/init_module.h"
 #include "library/equations_compiler/init_module.h"
+#include "library/inductive_compiler/init_module.h"
 #include "library/print.h"
 #include "library/vm/init_module.h"
 #include "library/compiler/init_module.h"
@@ -42,6 +43,7 @@ void initialize() {
     initialize_tactic_module();
     initialize_constructions_module();
     initialize_equations_compiler_module();
+    initialize_inductive_compiler_module();
     initialize_frontend_lean_module();
     initialize_frontend_smt2_module();
     initialize_vm_module();
@@ -51,6 +53,7 @@ void finalize() {
     finalize_vm_module();
     finalize_frontend_smt2_module();
     finalize_frontend_lean_module();
+    finalize_inductive_compiler_module();
     finalize_equations_compiler_module();
     finalize_constructions_module();
     finalize_tactic_module();
diff --git a/src/library/inductive_compiler/CMakeLists.txt b/src/library/inductive_compiler/CMakeLists.txt
new file mode 100644
index 0000000000..bb4e046c93
--- /dev/null
+++ b/src/library/inductive_compiler/CMakeLists.txt
@@ -0,0 +1,3 @@
+add_library(inductive_compiler OBJECT
+  init_module.cpp
+  )
diff --git a/src/library/inductive_compiler/init_module.cpp b/src/library/inductive_compiler/init_module.cpp
new file mode 100644
index 0000000000..87e72384bf
--- /dev/null
+++ b/src/library/inductive_compiler/init_module.cpp
@@ -0,0 +1,12 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Daniel Selsam
+*/
+namespace lean {
+
+void initialize_inductive_compiler_module() {}
+void finalize_inductive_compiler_module() {}
+
+}
diff --git a/src/library/inductive_compiler/init_module.h b/src/library/inductive_compiler/init_module.h
new file mode 100644
index 0000000000..6a02fa3263
--- /dev/null
+++ b/src/library/inductive_compiler/init_module.h
@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Daniel Selsam
+*/
+#pragma once
+namespace lean {
+void initialize_inductive_compiler_module();
+void finalize_inductive_compiler_module();
+}