diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt
index e23050c11f..12cc2a4af6 100644
--- a/collects/redex/private/reduction-semantics.rkt
+++ b/collects/redex/private/reduction-semantics.rkt
@@ -2255,7 +2255,7 @@
                  (if (procedure? goal) "satisfying" "equal to")
                  goal)
         (when (search-failure-cutoff? result)
-          (fprintf (current-error-port) " (but some terms were not unexplored)"))
+          (fprintf (current-error-port) " (but some terms were not explored)"))
         (newline (current-error-port))))))
 
 (define-syntax (test-predicate stx)
diff --git a/collects/redex/tests/tl-test.rkt b/collects/redex/tests/tl-test.rkt
index a09b87a5d4..2a5a2d671a 100644
--- a/collects/redex/tests/tl-test.rkt
+++ b/collects/redex/tests/tl-test.rkt
@@ -2455,7 +2455,7 @@
     
     (define (equal-to-7 x) (= x 7))
     (test (capture-output (test-->>∃ #:steps 5 1+ 0 equal-to-7))
-          #rx"^FAILED .*\nno reachable term satisfying #<procedure:equal-to-7> \\(but some terms were not unexplored\\)\n$")
+          #rx"^FAILED .*\nno reachable term satisfying #<procedure:equal-to-7> \\(but some terms were not explored\\)\n$")
     
     (test (capture-output (test-->>∃ 1+ 0 7)) "")
     (test (capture-output (test-->>E 1+ 0 7)) "")