diff --git a/tests/lean/inductive_sorry.lean b/tests/lean/inductive_sorry.lean
deleted file mode 100644
index 1c6cdc314c..0000000000
--- a/tests/lean/inductive_sorry.lean
+++ /dev/null
@@ -1,12 +0,0 @@
-inductive foo (A : sorry → ℕ)
-| mk : foo
-
-inductive foo : sorry → ℕ
-| mk : foo 0
-
-inductive foo
-| mk : sorry → foo
-
-structure foo (A : sorry → ℕ) := (x : ℕ)
-
-structure foo : Type := (x : bool → sorry)
diff --git a/tests/lean/inductive_sorry.lean.expected.out b/tests/lean/inductive_sorry.lean.expected.out
deleted file mode 100644
index 9e23205657..0000000000
--- a/tests/lean/inductive_sorry.lean.expected.out
+++ /dev/null
@@ -1,5 +0,0 @@
-inductive_sorry.lean:1:0: error: type of parameter 'A' contains 'sorry'
-inductive_sorry.lean:4:0: error: type of parameter 'foo' contains 'sorry'
-inductive_sorry.lean:7:0: error: constructor 'foo.mk' contains 'sorry'
-inductive_sorry.lean:10:0: error: type of parameter 'A' contains 'sorry'
-inductive_sorry.lean:12:0: error: field 'x' contains 'sorry'