diff --git a/library/init/default.lean b/library/init/default.lean
index 69dcbfd8d1..de062e2e9c 100644
--- a/library/init/default.lean
+++ b/library/init/default.lean
@@ -6,4 +6,4 @@ Authors: Leonardo de Moura
 prelude
 import init.core init.control init.data.basic init.version
 import init.function init.util init.coe init.wf init.meta
-import init.meta.well_founded_tactics init.data init.io
+import init.data init.io
diff --git a/library/init/meta/well_founded_tactics.lean b/library/init/meta/well_founded_tactics.lean
deleted file mode 100644
index 3bf098eacf..0000000000
--- a/library/init/meta/well_founded_tactics.lean
+++ /dev/null
@@ -1,23 +0,0 @@
-/-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import init.meta
-
-/-- Argument for using_well_founded
-
-  The tactic `rel_tac` has to synthesize an element of type (has_well_founded A).
-  The two arguments are: a local representing the function being defined by well
-  founded recursion, and a list of recursive equations.
-  The equations can be used to decide which well founded relation should be used.
-
-  The tactic `dec_tac` has to synthesize decreasing proofs.
--/
-meta structure well_founded_tactics :=
-(rel_tac : expr → list expr → tactic unit := λ _ _, tactic.apply_instance)
-(dec_tac : tactic unit := tactic.assumption)
-
-meta def well_founded_tactics.default : well_founded_tactics :=
-{}