diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp index 2cc83fcdb5..02375a1f69 100644 --- a/src/frontends/lean/inductive_cmds.cpp +++ b/src/frontends/lean/inductive_cmds.cpp @@ -28,7 +28,6 @@ Authors: Daniel Selsam, Leonardo de Moura #include "library/reducible.h" #include "library/class.h" #include "library/trace.h" -#include "library/app_builder.h" #include "library/type_context.h" #include "library/documentation.h" #include "library/constants.h"