diff --git a/doc/README.agda b/doc/README.agda
index b1c969fd71..f17fb75eb7 100644
--- a/doc/README.agda
+++ b/doc/README.agda
@@ -241,11 +241,6 @@ import README.Debug.Trace
 
 import README.Nary
 
--- Explaining the inspect idiom: use case, equivalent handwritten
--- auxiliary definitions, and implementation details.
-
-import README.Inspect
-
 -- Explaining how to use the automatic solvers
 
 import README.Tactic.MonoidSolver
diff --git a/doc/README/Inspect.agda b/doc/README/Inspect.agda
index 2199a499c8..406e47e56b 100644
--- a/doc/README/Inspect.agda
+++ b/doc/README/Inspect.agda
@@ -1,14 +1,23 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Explaining how to use the inspect idiom and elaborating on the way
--- it is implemented in the standard library.
+-- This module is DEPRECATED.
+--
+-- The record type `Reveal_·_is_`, and its principal mode of use,
+-- via the `inspect` function described below, have been deprecated
+-- in favour of the `with ... in ...` syntax. See the documentation
+--
+-- https://agda.readthedocs.io/en/v2.9.0/language/with-abstraction.html#with-abstraction-equality
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
 module README.Inspect where
 
+{-# WARNING_ON_IMPORT
+"README.Inspect was deprecated in v2.4."
+#-}
+
 open import Data.Nat.Base
 open import Data.Nat.Properties
 open import Data.Product.Base using (_×_; _,_)