diff --git a/tests/elab/printDecls.lean b/tests/elab/printDecls.lean
deleted file mode 100644
index 6006ce421f..0000000000
--- a/tests/elab/printDecls.lean
+++ /dev/null
@@ -1,26 +0,0 @@
-import Lean
-
-open Lean
-open Lean.Meta
-
--- Return true if `declName` should be ignored
-def shouldIgnore (declName : Name) : Bool :=
-  declName.isInternal
-  || match declName with
-     | .str _ s => "match_".isPrefixOf s || "proof_".isPrefixOf s || "eq_".isPrefixOf s
-     | _ => true
-
--- Print declarations that have the given prefix.
-def printDecls (pre : Name) : MetaM Unit := do
-  let cs := (← getEnv).constants
-  cs.forM fun declName info => do
-    if pre.isPrefixOf declName && !shouldIgnore declName then
-      if let some docString ← findDocString? (← getEnv) declName then
-        IO.println s!"/-- {docString} -/\n{declName} : {← ppExpr info.type}"
-      else
-        IO.println s!"{declName} : {← ppExpr info.type}"
-
-#eval printDecls `Array
-#eval printDecls `List
-#eval printDecls `Bool
-#eval printDecls `Lean.Elab
diff --git a/tests/elab/printDecls.lean.out.ignored b/tests/elab/printDecls.lean.out.ignored
deleted file mode 100644
index e69de29bb2..0000000000