diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 09138bf7ed..7d7f55ce62 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -137,9 +137,6 @@ It can also be written as `()`.
 /-- Marker for information that has been erased by the code generator. -/
 unsafe axiom lcErased : Type
 
-/-- "Any" type in the simpler type system used by the code generator. -/
-unsafe axiom lcAny : Type
-
 /--
 Auxiliary unsafe constant used by the Compiler when erasing proofs from code.
 
diff --git a/tests/lean/lcnfTypes.lean b/tests/lean/lcnfTypes.lean
index 3fbf4f118f..f5f35191d6 100644
--- a/tests/lean/lcnfTypes.lean
+++ b/tests/lean/lcnfTypes.lean
@@ -1,7 +1,6 @@
 import Lean
 
 notation "◾" => lcErased
-notation "⊤" => lcAny
 
 open Lean Compiler LCNF Meta