diff --git a/collects/redex/private/term-fn.ss b/collects/redex/private/term-fn.ss
index 5abe326149..26d246660a 100644
--- a/collects/redex/private/term-fn.ss
+++ b/collects/redex/private/term-fn.ss
@@ -9,4 +9,4 @@
   (make-struct-type 'term-fn #f 1 0))
 (define term-fn-get-id (make-struct-field-accessor term-fn-get 0))
 
-(define-struct term-id (id))
+(define-struct term-id (id depth))
diff --git a/collects/redex/private/term-test.ss b/collects/redex/private/term-test.ss
index 8f38959677..81ab570a52 100644
--- a/collects/redex/private/term-test.ss
+++ b/collects/redex/private/term-test.ss
@@ -1,4 +1,4 @@
-(module term-test mzscheme
+(module term-test scheme
   (require "term.ss"
            "matcher.ss"
            "test-util.ss")
@@ -67,10 +67,7 @@
           (term ((in-hole E x) ...)))
         (term (1 2 3)))
   
-  (fprintf (current-error-port) "term-test.ss commented out test that fails; matches PR 8765\n")
-  
-  #;
-  (test (term-let-fn ((metafun (λ (x) x)))
+  (test (term-let-fn ((metafun car))
                      (term-let ((x 'whatever)
                                 ((y ...) '(4 5 6)))
                        (term (((metafun x) y) ...))))
@@ -81,4 +78,26 @@
                        (term ((y (metafun 1)) ...))))
         '((4 1) (5 1) (6 1)))
   
+  (test (term-let-fn ((f (compose add1 car)))
+                     (term-let (((x ...) '(1 2 3))
+                                ((y ...) '(a b c)))
+                               (term (((f x) y) ...))))
+        '((2 a) (3 b) (4 c)))
+  
+  (test (term-let-fn ((f (curry foldl + 0)))
+                     (term-let (((x ...) '(1 2 3)))
+                               (term (f x ...))))
+        6)
+  
+  (test (term-let-fn ((f (compose add1 car)))
+                     (term-let (((x ...) '(1 2 3))
+                                (((y ...) ...) '((a b c) (d e f) (g h i))))
+                               (term ((((f x) y) ...) ...))))
+        '(((2 a) (3 b) (4 c)) ((2 d) (3 e) (4 f)) ((2 g) (3 h) (4 i))))
+  
+  (test (term-let-fn ((f (curry foldl + 0)))
+                     (term-let ((((x ...) ...) '((1 2) (3 4 5) (6))))
+                               (term ((f x ...) ...))))
+        '(3 12 6))
+  
   (print-tests-passed 'term-test.ss))
diff --git a/collects/redex/private/term.ss b/collects/redex/private/term.ss
index 98654bc6a8..cc6482a45a 100644
--- a/collects/redex/private/term.ss
+++ b/collects/redex/private/term.ss
@@ -5,7 +5,10 @@
                      syntax/private/util/misc)
          "matcher.ss")
 
-(provide term term-let term-let/error-name term-let-fn term-define-fn)
+(provide term term-let term-let/error-name term-let-fn term-define-fn hole in-hole)
+
+(define-syntax (hole stx) (raise-syntax-error 'hole "used outside of term"))
+(define-syntax (in-hole stx) (raise-syntax-error 'in-hole "used outside of term"))
 
 (define (with-syntax* stx)
   (syntax-case stx ()
@@ -15,112 +18,95 @@
 (define-syntax (term stx)
   (syntax-case stx ()
     [(_ arg)
-     #`(term-let-fn ((#,(datum->syntax stx 'in-hole)
-                      (λ (x) 
-                        (unless (and (list? x)
-                                     (= 2 (length x)))
-                          (error 'in-hole "expected two arguments, got ~s" x))
-                        (apply plug x))))
-                    (term/private arg))]))
+    #`(term/private arg)]))
 
 (define-syntax (term/private orig-stx)
   (define outer-bindings '())
   
   (define (rewrite stx)
-    (let-values ([(rewritten has-term-let-bound-id?)
-                  (rewrite/has-term-let-bound-id? stx)])
+    (let-values ([(rewritten _) (rewrite/max-depth stx 0)])
       rewritten))
   
-  (define (rewrite/has-term-let-bound-id? stx)
-    (let loop ([stx stx]
-               [depth 0])
-      (syntax-case stx (unquote unquote-splicing in-hole hole)
-        [(metafunc-name arg ...)
-         (and (identifier? (syntax metafunc-name))
-              (term-fn? (syntax-local-value (syntax metafunc-name) (λ () #f))))
-         (let-values ([(rewritten has-term-let-bound-id?) (loop (syntax (arg ...)) depth)])
-           (let ([term-fn (syntax-local-value/catch (syntax metafunc-name) (λ (x) #t))])
-             (with-syntax ([f (term-fn-get-id term-fn)])
-               (cond
-                 [has-term-let-bound-id?
-                  (with-syntax ([(f-results) (generate-temporaries '(f-results))])
-                    (let d-loop ([arg-dots rewritten]
-                                 [fres (syntax f-results)]
-                                 [func (syntax (lambda (x) (f (syntax->datum x))))]
-                                 [depth depth])
-                      (cond
-                        [(zero? depth) 
-                         (let ([res 
-                                (with-syntax ([fres fres]
-                                              [func func]
-                                              [arg-dots arg-dots])
-                                  (set! outer-bindings (cons (syntax [fres (func (quasisyntax arg-dots))])
-                                                             outer-bindings))
-                                  (syntax f-results))])
-                           (values res #t))]
-                        [else 
-                         (with-syntax ([dots (quote-syntax ...)]
-                                       [arg-dots arg-dots]
-                                       [fres fres])
-                           (d-loop (syntax (arg-dots dots))
-                                   (syntax (fres dots))
-                                   (with-syntax ([f func])
-                                     (syntax (lambda (l) (map f (syntax->list l)))))
-                                   (- depth 1)))])))]
-                 [else
-                  (with-syntax ([rewritten rewritten])
-                    (values (syntax/loc stx (unsyntax (f (syntax->datum (quasisyntax rewritten)))))
-                            #f))]))))]
-        [f
-         (and (identifier? (syntax f))
-              (term-fn? (syntax-local-value (syntax f) (λ () #f))))
-         (raise-syntax-error 'term "metafunction must be in an application" orig-stx stx)]
-        [x
-         (and (identifier? (syntax x))
-              (term-id? (syntax-local-value (syntax x) (λ () #f))))
-         (values (term-id-id (syntax-local-value/catch (syntax x) (λ (x) #t))) #t)]
-        [(unquote x)
-         (values (syntax (unsyntax x)) #f)]
-        [(unquote . x)
-         (raise-syntax-error 'term "malformed unquote" orig-stx stx)]
-        [(unquote-splicing x)
-         (values (syntax (unsyntax-splicing x)) #f)]
-        [(unquote-splicing . x)
-         (raise-syntax-error 'term "malformed unquote splicing" orig-stx stx)]
-        [(in-hole id body)
-         (values (syntax (unsyntax (plug (term id) (term body)))) #f)]
-        [(in-hole . x)
-         (raise-syntax-error 'term "malformed in-hole" orig-stx stx)]
-        [hole (values (syntax (unsyntax the-hole)) #f)]
-        
-        
-        [() (values stx #f)]
-        [(x ... . y)
-         (not (null? (syntax->list #'(x ...))))
-         (let-values ([(x-rewrite has-term-let-bound-id?)
-                       (let i-loop ([xs (syntax->list (syntax (x ...)))])
-                         (cond
-                           [(null? xs) (loop #'y depth)]
-                           [else
-                            (let ([new-depth (if (and (not (null? (cdr xs)))
-                                                      (identifier? (cadr xs))
-                                                      (free-identifier=? (quote-syntax ...)
-                                                                         (cadr xs)))
-                                                 (+ depth 1)
-                                                 depth)])
-                              (let-values ([(fst fst-has-term-let-bound-id?)
-                                            (loop (car xs) new-depth)]
-                                           [(rst rst-has-term-let-bound-id?)
-                                            (i-loop (cdr xs))])
-                                (values (cons fst rst)
-                                        (or fst-has-term-let-bound-id?
-                                            rst-has-term-let-bound-id?))))]))])
-           
-           (with-syntax ([x-rewrite x-rewrite])
-             (values (syntax/loc stx x-rewrite)
-                     has-term-let-bound-id?)))]
-        
-        [_ (values stx #f)])))
+  (define (rewrite-application fn args depth)
+    (let-values ([(rewritten max-depth) (rewrite/max-depth args depth)])
+      (let ([result-id (car (generate-temporaries '(f-results)))])
+        (with-syntax ([fn fn])
+          (let loop ([func (syntax (λ (x) (fn (syntax->datum x))))]
+                     [args rewritten]
+                     [res result-id]
+                     [args-depth (min depth max-depth)])
+            (with-syntax ([func func]
+                          [args args]
+                          [res res])
+              (if (zero? args-depth)
+                  (begin
+                    (set! outer-bindings 
+                          (cons (syntax [res (func (quasisyntax args))])
+                                outer-bindings))
+                    (values result-id (min depth max-depth)))
+                  (loop (syntax (λ (l) (map func (syntax->list l))))
+                        (syntax (args (... ...)))
+                        (syntax (res (... ...)))
+                        (sub1 args-depth)))))))))
+  
+  (define (rewrite/max-depth stx depth)
+    (syntax-case stx (unquote unquote-splicing in-hole hole)
+      [(metafunc-name arg ...)
+       (and (identifier? (syntax metafunc-name))
+            (term-fn? (syntax-local-value (syntax metafunc-name) (λ () #f))))
+       (rewrite-application (term-fn-get-id (syntax-local-value/catch (syntax metafunc-name) (λ (x) #t)))
+                            (syntax (arg ...))
+                            depth)]
+      [f
+       (and (identifier? (syntax f))
+            (term-fn? (syntax-local-value (syntax f) (λ () #f))))
+       (raise-syntax-error 'term "metafunction must be in an application" orig-stx stx)]
+      [x
+       (and (identifier? (syntax x))
+            (term-id? (syntax-local-value (syntax x) (λ () #f))))
+       (let ([id (syntax-local-value/catch (syntax x) (λ (x) #t))])
+         (values (term-id-id id) (term-id-depth id)))]
+      [(unquote x)
+       (values (syntax (unsyntax x)) 0)]
+      [(unquote . x)
+       (raise-syntax-error 'term "malformed unquote" orig-stx stx)]
+      [(unquote-splicing x)
+       (values (syntax (unsyntax-splicing x)) 0)]
+      [(unquote-splicing . x)
+       (raise-syntax-error 'term "malformed unquote splicing" orig-stx stx)]
+      [(in-hole id body)
+       (rewrite-application (syntax (λ (x) (apply plug x))) (syntax (id body)) depth)]
+      [(in-hole . x)
+       (raise-syntax-error 'term "malformed in-hole" orig-stx stx)]
+      [hole (values (syntax (unsyntax the-hole)) 0)]
+      
+      
+      [() (values stx 0)]
+      [(x ... . y)
+       (not (null? (syntax->list #'(x ...))))
+       (let-values ([(x-rewrite max-depth)
+                     (let i-loop ([xs (syntax->list (syntax (x ...)))])
+                       (cond
+                         [(null? xs) (rewrite/max-depth #'y depth)]
+                         [else
+                          (let ([new-depth (if (and (not (null? (cdr xs)))
+                                                    (identifier? (cadr xs))
+                                                    (free-identifier=? (quote-syntax ...)
+                                                                       (cadr xs)))
+                                               (+ depth 1)
+                                               depth)])
+                            (let-values ([(fst fst-max-depth)
+                                          (rewrite/max-depth (car xs) new-depth)]
+                                         [(rst rst-max-depth)
+                                          (i-loop (cdr xs))])
+                              (values (cons fst rst)
+                                      (max fst-max-depth rst-max-depth))))]))])
+         
+         (with-syntax ([x-rewrite x-rewrite])
+           (values (syntax/loc stx x-rewrite)
+                   max-depth)))]
+      
+      [_ (values stx 0)]))
   
   (syntax-case orig-stx ()
     [(_ arg)
@@ -157,38 +143,48 @@
 (define-syntax (term-let/error-name stx)
   (syntax-case stx ()
     [(_ error-name ([x1 rhs1] [x rhs] ...) body1 body2 ...)
-     (let-values ([(orig-names new-names new-x1)
-                   (let loop ([stx #'x1])
-                     (syntax-case stx ()
+     (let-values ([(orig-names new-names depths new-x1)
+                   (let loop ([stx #'x1] [depth 0])
+                     (define ((combine orig-names new-names depths new-pat)
+                              orig-names* new-names* depths* new-pat*)
+                       (values (append orig-names orig-names*)
+                               (append new-names new-names*)
+                               (append depths depths*)
+                               (cons new-pat new-pat*)))
+                     (syntax-case stx (...)
                        [x 
                         (and (identifier? #'x)
                              (not (free-identifier=? (quote-syntax ...) #'x)))
                         (let ([new-name (car (generate-temporaries (list #'x)))])
                           (values (list #'x)
                                   (list new-name)
+                                  (list depth)
                                   new-name))]
-                       [(x ...)
-                        (let l-loop ([lst (syntax->list #'(x ...))])
-                          (cond
-                            [(null? lst)
-                             (values '() '() '())]
-                            [else
-                             (let-values ([(hd-orig-names hd-new-names hd-new-pattern)
-                                           (loop (car lst))]
-                                          [(tl-orig-names tl-new-names tl-new-pattern)
-                                           (l-loop (cdr lst))])
-                               (values (append hd-orig-names tl-orig-names)
-                                       (append hd-new-names tl-new-names)
-                                       (cons hd-new-pattern tl-new-pattern)))]))]
+                       [(x (... ...) . xs)
+                        (let-values ([(orig-names new-names depths new-pat)
+                                      (call-with-values
+                                       (λ () (loop #'xs depth))
+                                       (call-with-values
+                                        (λ () (loop #'x (add1 depth)))
+                                        combine))])
+                          (values orig-names new-names depths 
+                                  (list* (car new-pat) #'(... ...) (cdr new-pat))))]
+                       [(x . xs)
+                        (call-with-values
+                         (λ () (loop #'xs depth))
+                         (call-with-values
+                          (λ () (loop #'x depth))
+                          combine))]
                        [_
-                        (values '() '() stx)]))])
+                        (values '() '() '() stx)]))])
        (with-syntax ([(orig-names ...) orig-names]
                      [(new-names ...) new-names]
+                     [(depths ...) depths]
                      [new-x1 new-x1])
          (syntax
           (syntax-case rhs1 ()
             [new-x1 
-             (let-syntax ([orig-names (make-term-id #'new-names)] ...)
+             (let-syntax ([orig-names (make-term-id #'new-names (syntax-e #'depths))] ...)
                (term-let/error-name error-name ((x rhs) ...) body1 body2 ...))]
             [_ (error 'error-name "term ~s does not match pattern ~s" rhs1 'x1)]))))]
     [(_ error-name () body1 body2 ...)
diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl
index 78403d6e8b..1988cd8f2e 100644
--- a/collects/redex/redex.scrbl
+++ b/collects/redex/redex.scrbl
@@ -485,6 +485,14 @@ for two @scheme[term-let]-bound identifiers bound to lists of
 different lengths to appear together inside an ellipsis.
 }
 
+@defidform[hole]{ Recognized specially within
+  @scheme[term]. A @scheme[hole] form is an
+  error elsewhere.  }
+
+@defidform[in-hole]{ Recognized specially within
+  @scheme[reduction-relation]. An @scheme[in-hole] form is an
+  error elsewhere.  }
+
 @defform/subs[(term-let ([tl-pat expr] ...) body)
               ([tl-pat identifier (tl-pat-ele ...)]
                [tl-pat-ele tl-pat (code:line tl-pat ... (code:comment "a literal ellipsis"))])]{
diff --git a/collects/redex/reduction-semantics.ss b/collects/redex/reduction-semantics.ss
index 067a2e443a..fc8a9ff9d0 100644
--- a/collects/redex/reduction-semantics.ss
+++ b/collects/redex/reduction-semantics.ss
@@ -11,6 +11,7 @@
 
 (provide reduction-relation 
          --> fresh with ;; keywords for reduction-relation
+         hole in-hole ;; keywords for term
          extend-reduction-relation
          reduction-relation?
          
diff --git a/doc/release-notes/redex/HISTORY.txt b/doc/release-notes/redex/HISTORY.txt
index b77a1990cb..887b6f2499 100644
--- a/doc/release-notes/redex/HISTORY.txt
+++ b/doc/release-notes/redex/HISTORY.txt
@@ -1,11 +1,12 @@
-v4.2.3
-
   * added support for collecting metafunction coverage, using the
     'relation-coverage' parameter. This includes a backwards
     incompatible change: the parameter's value is now a list of
     coverage structures, to allow coverage collection for multiple 
     metafunctions and reduction relations at once.
 
+  * redex/reduction-semantics exports the names `hole' and `in-hole'
+    (and `term' no longer captures those names).
+
   * minor bug fixes
 
 v4.2.2