From 7106bcf7a5f8a97f5dcf6de0a58efe031f9e7a9d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 15 Dec 2017 11:35:34 -0800
Subject: [PATCH] chore(frontends/lean/inductive_cmds): remove `app_builder`
 dependency

---
 src/frontends/lean/inductive_cmds.cpp | 1 -
 1 file changed, 1 deletion(-)

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"