diff --git a/collects/redex/examples/church.ss b/collects/redex/examples/church.ss
index b3152a11b5..06aa2fa0ad 100644
--- a/collects/redex/examples/church.ss
+++ b/collects/redex/examples/church.ss
@@ -5,18 +5,17 @@
 
 (define-language lang
   (e (lambda (x) e)
-     (let (x e) e)
-     (app e e)
+     (e e)
      (+ e e)
      number
      x)
-  (e-ctxt (lambda (x) e-ctxt)
-          a-ctxt)
-  (a-ctxt (let (x a-ctxt) e)
-          (app a-ctxt e)
-          (app x a-ctxt)
+  (ctxt (ctxt e)
+          (v ctxt)
+          (+ ctxt e)
+          (+ v ctxt)
           hole)
   (v (lambda (x) e)
+     number
      x)
   (x variable))
 
@@ -47,11 +46,4 @@
       (subst (x_1 e_1 e_3)))]
   [(subst (x_1 e_1 number_1)) number_1])
 
-(traces reductions
-        '(let (plus (lambda (m) 
-                      (lambda (n) 
-                        (lambda (s)
-                          (lambda (z)
-                            (app (app m s) (app (app n s) z)))))))
-           (let (two (lambda (s) (lambda (z) (app s (app s z)))))
-             (app (app plus two) two))))
+(apply-reduction-relation reductions `(app (lambda (x) x) (lambda (x) x)))
diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl
index feebc5593b..122d6f7e88 100644
--- a/collects/redex/redex.scrbl
+++ b/collects/redex/redex.scrbl
@@ -857,7 +857,7 @@ terminate (it does terminate if the only infinite reduction paths are cyclic).
   error elsewhere.  }
 
 @defidform[fresh]{ Recognized specially within
-  @scheme[reduction-relation]. A @scheme[-->] form is an
+  @scheme[reduction-relation]. A @scheme[fresh] form is an
   error elsewhere.  }
 
 @defidform[with]{ Recognized specially within