diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt
index d61d81bf12..390d4f9619 100644
--- a/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt
+++ b/pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt
@@ -147,8 +147,10 @@
                  [res-term-stx #`(#,jf-id #,@args-stx)]
                  [property #`(bind-prop
                                (λ (bindings)
-                                 (term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
-                                           #,property)))])
+                                 #,(bind-pattern-names 'redex-check
+                                                       #'(names/ellipses ...)
+                                                       #'((lookup-binding bindings 'names) ...)
+                                                       property)))])
                 (quasisyntax/loc orig-stx
                   (let ([term-match (λ (generated)
                                       (cond [(test-match #,lang res-term-stx generated) => values]
@@ -183,9 +185,12 @@
                  [show (show-message orig-stx)]
                  [property #`(bind-prop
                                (λ (bindings)
-                                 (term-let ([lhs-names/ellipses (lookup-binding bindings 'lhs-names)] ...
-                                            [rhs-names/ellipses (lookup-binding bindings 'rhs-names)] ...)
-                                           #,property)))])
+                                 #,(bind-pattern-names 'redex-check
+                                                       #'(lhs-names/ellipses ... 
+                                                          rhs-names/ellipses ...)
+                                                       #'((lookup-binding bindings 'lhs-names) ...
+                                                          (lookup-binding bindings 'rhs-names) ...)
+                                                       property)))])
                 (quasisyntax/loc orig-stx
                   (let ([term-match (λ (generated)
                                       (cond [(test-match #,lang res-term-stx generated) => values]
@@ -214,8 +219,10 @@
       (parse-redex-check-kw-args kw-args orig-stx form)) 
     (with-syntax ([property #`(bind-prop
                                (λ (bindings)
-                                 (term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
-                                           #,property)))])
+                                 #,(bind-pattern-names 'redex-check
+                                                       #'(name/ellipses ...)
+                                                       #'((lookup-binding bindings 'name) ...)
+                                                       property)))])
       (quasisyntax/loc orig-stx
         (let ([att #,attempts-stx]
               [ret #,retries-stx]
diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt
index 0b588d9490..a067104907 100644
--- a/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt
+++ b/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt
@@ -154,8 +154,10 @@
                  (λ (bindings)
                    (let ([x (lookup-binding bindings 'names)] ...)
                      (and binding-constraints ...
-                          (term-let ([names/ellipses x] ...) 
-                                    #,rest-body)))))))))]
+                          #,(bind-pattern-names orig-name
+                                                #'(names/ellipses ...)
+                                                #'(x ...)
+                                                rest-body)))))))))]
        [((-side-condition s ...) y ...)
         (side-condition-keyword? #'-side-condition)
         (if side-condition-unquoted?
@@ -239,8 +241,10 @@
                  (λ (bindings #,(if jf-results-id jf-results-id '_ignored))
                    (let ([temp (lookup-binding bindings 'output-name)] ...)
                      (and binding-constraint ...
-                          (term-let ([output-name/ellipsis temp] ...)
-                                    #,rest-body))))))))]))))
+                          #,(bind-pattern-names orig-name
+                                                #'(output-name/ellipsis ...)
+                                                #'(temp ...)
+                                                rest-body))))))))]))))
 
 (define (judgment-form-bind-withs/proc lang output-pattern output under-ellipsis? old-maps do-something)
   (let ([compiled-pattern (compile-pattern lang output-pattern #t)])
@@ -816,8 +820,10 @@
                        compiled-lhs
                        input
                        (λ (bnds)
-                         (term-let ([names/ellipses (lookup-binding bnds 'names)] ...)
-                                   #,body))
+                         #,(bind-pattern-names 'judgment-form
+                                               #'(names/ellipses ...)
+                                               #'((lookup-binding bnds 'names) ...)
+                                               body))
                        #,(if output-contracts
                              #`(λ (output)
                                  (check-judgment-form-contract '#,name output compiled-output-ctcs 'O '#,mode))
diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt
index fc6a959a98..c2921b9527 100644
--- a/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt
+++ b/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt
@@ -47,17 +47,24 @@
                            (syntax->list (syntax (pattern ...))))]
                      [(cp-x ...) (generate-temporaries #'(pattern ...))]
                      [make-matcher make-matcher])
-         #'(begin
-             syncheck-expr ...
-             (make-matcher
-              'form-name lang 
-              (list 'pattern ...)
-              (list (compile-pattern lang `side-conditions-rewritten #t) ...)
-              (list (λ (match)
-                      (term-let/error-name 
-                       form-name
-                       ([names/ellipses (lookup-binding (mtch-bindings match) 'names)] ...)
-                       rhs)) ...)))))]))
+         (with-syntax ([(mtch-procs ...)
+                        (for/list ([names/ellipses (in-list (syntax->list #'((names/ellipses ...) ...)))]
+                                   [names (in-list (syntax->list #'((names ...) ...)))]
+                                   [rhs (in-list (syntax->list #'(rhs ...)))])
+                          (with-syntax ([(names ...) names])
+                            #`(λ (match)
+                                #,(bind-pattern-names 
+                                   #'form-name 
+                                   names/ellipses
+                                   #'((lookup-binding (mtch-bindings match) 'names) ...)
+                                   rhs))))])
+           #`(begin
+               syncheck-expr ...
+               (make-matcher
+                'form-name lang 
+                (list 'pattern ...)
+                (list (compile-pattern lang `side-conditions-rewritten #t) ...)
+                (list mtch-procs ...))))))]))
 
 (define-syntax (term-match/single stx)
   (term-matcher stx #'term-match/single/proc))
@@ -683,10 +690,12 @@
                      'lhs-frm-id
                      'lhs-to-id
                      `side-conditions-rewritten
-                     (λ (bindings rhs-binder)
-                       (term-let ([lhs-to-id rhs-binder]
-                                  [names/ellipses (lookup-binding bindings 'names)] ...)
-                                 (term rhs-to #:lang lang)))
+                     (λ (bindings rhs-binder) 
+                       (term-let ([lhs-to-id rhs-binder])
+                                 #,(bind-pattern-names 'reduction-relation
+                                                       #'(names/ellipses ...)
+                                                       #'((lookup-binding bindings 'names) ...)
+                                                       #'(term rhs-to #:lang lang))))
                      #,child-proc
                      `fresh-rhs-from)))
               (get-choices stx orig-name bm #'lang
@@ -779,13 +788,16 @@
                       [body-code body-code])
           #`(begin
               lhs-syncheck-expr
-              (build-rewrite-proc/leaf `side-conditions-rewritten
-                                       (λ (main-exp bindings)
-                                         (term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
-                                                   body-code))
-                                       lhs-source
-                                       name
-                                       (λ (lang-id2) `lhs-w/extras))))))
+              (build-rewrite-proc/leaf 
+               `side-conditions-rewritten
+               (λ (main-exp bindings)
+                 #,(bind-pattern-names 'reduction-relation
+                                       #'(names/ellipses ...)
+                                       #'((lookup-binding bindings 'names) ...)
+                                       #'body-code))
+               lhs-source
+               name
+               (λ (lang-id2) `lhs-w/extras))))))
     
     (define (process-extras stx orig-name name-table extras)
       (let* ([the-name #f]
@@ -1085,12 +1097,15 @@
           (let ([ans (match-pattern cpat exp)])
             (and ans
                  (map (λ (m) (make-match (sort-bindings 
-                                          (filter (λ (x) (memq (bind-name x) binders))
+                                          (filter (λ (x) (and (memq (bind-name x) binders)
+                                                              (not-ellipsis-name (bind-name x))))
                                                   (bindings-table (mtch-bindings m))))))
                       ans))))))
   (if name
       (procedure-rename redex-match-proc name)
       redex-match-proc))
+(define (not-ellipsis-name x)
+  (not (regexp-match? #rx"^[.][.][.]" (symbol->string x))))
 
 (define (sort-bindings bnds)
   (sort
@@ -1704,6 +1719,10 @@
                 "cannot use pattern language keyword as a non-terminal name")
     (check-each names (λ (x) (regexp-match? #rx"_" (symbol->string (syntax-e x))))
                 "cannot use _ in a non-terminal name")
+    (check-each names (λ (x) (regexp-match? #rx"^[.][.][.]$" (symbol->string (syntax-e x))))
+                "cannot name a non-terminal `...'")
+    (check-each names (λ (x) (regexp-match? #rx"^[.][.][.]_" (symbol->string (syntax-e x))))
+                "cannot start a non-terminal name with `..._'")
     
     (when (null? prods)
       (raise-syntax-error #f "expected at least one production to follow" 
diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/rewrite-side-conditions.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/rewrite-side-conditions.rkt
index e03ece49a2..c0de07df96 100644
--- a/pkgs/redex-pkgs/redex-lib/redex/private/rewrite-side-conditions.rkt
+++ b/pkgs/redex-pkgs/redex-lib/redex/private/rewrite-side-conditions.rkt
@@ -14,7 +14,8 @@
            (rename-out [binds? id-binds?])
            raise-ellipsis-depth-error
            make-language-id
-           language-id-nts)
+           language-id-nts
+           bind-pattern-names)
   
   (provide (struct-out id/depth))
   
@@ -59,6 +60,11 @@
     ;; hash[sym -o> (listof stx)]
     (define var-locs-table (make-hash))
     
+    ;; hash[sym -o> sym]
+    ;; tells the original names for any given repeat to be replaced after
+    ;; normalization and checking has finished
+    (define original-repeat-names (make-hash))
+    
     (define (record-binder pat-stx under under-mismatch-ellipsis)
       (define pat-sym (syntax->datum pat-stx))
       (hash-set! var-locs-table pat-sym (cons pat-stx (hash-ref var-locs-table pat-sym '())))
@@ -288,24 +294,29 @@
                                           orig-stx
                                           (cadr terms)
                                           (list (caddr terms))))
-                    (define ellipsis-sym (syntax-e (cadr terms)))
-                    (define ellipsis-pre-str (symbol->string ellipsis-sym))
+                    (define ellipsis-pre-sym (syntax-e (cadr terms)))
+                    (define ellipsis-pre-str (symbol->string ellipsis-pre-sym))
                     (define mismatch? (regexp-match? #rx"^[.][.][.]_!_" ellipsis-pre-str))
-                    (define ellipsis-str (cond
-                                           [mismatch?
-                                            (set! ellipsis-number (+ ellipsis-number 1))
-                                            (format "..._r~a" ellipsis-number)]
-                                           [(regexp-match? #rx"^[.][.][.]_r" ellipsis-pre-str)
-                                            (string-append (substring ellipsis-str 0 4)
-                                                           "r"
-                                                           (substring ellipsis-str 
-                                                                      4
-                                                                      (string-length ellipsis-str)))]
-                                           [(regexp-match? #rx"^[.][.][.]_" ellipsis-pre-str) 
-                                            ellipsis-pre-str]
-                                           [else 
-                                            (set! ellipsis-number (+ ellipsis-number 1))
-                                            (format "..._r~a" ellipsis-number)]))
+                    (define-values (ellipsis-str was-named-ellipsis?)
+                      (cond
+                        [mismatch?
+                         (set! ellipsis-number (+ ellipsis-number 1))
+                         (values (format "..._r~a" ellipsis-number) #f)]
+                        [(regexp-match? #rx"^[.][.][.]_r" ellipsis-pre-str)
+                         (values (string-append (substring ellipsis-str 0 4)
+                                                "r"
+                                                (substring ellipsis-str 
+                                                           4
+                                                           (string-length ellipsis-str)))
+                                 #t)]
+                        [(regexp-match? #rx"^[.][.][.]_" ellipsis-pre-str) 
+                         (values ellipsis-pre-str #t)]
+                        [else 
+                         (set! ellipsis-number (+ ellipsis-number 1))
+                         (values (format "..._r~a" ellipsis-number) #f)]))
+                    (define ellipsis-sym (string->symbol ellipsis-str))
+                    (when was-named-ellipsis? 
+                      (hash-set! original-repeat-names ellipsis-sym ellipsis-pre-sym))
                     (define ellipsis+name (datum->syntax
                                            (cadr terms)
                                            (string->symbol ellipsis-str)
@@ -318,11 +329,13 @@
                                 (cons (syntax-e (cadr terms)) under-mismatch-ellipsis)
                                 under-mismatch-ellipsis)))
                     (define-values (rst-terms rst-vars) (t-loop (cddr terms)))
-                    (values (cons `(repeat ,fst-term 
-                                           ,ellipsis+name
-                                           ,(if mismatch? (cadr terms) #f))
+                    (values (cons `(repeat ,fst-term ,ellipsis+name ,(if mismatch? (cadr terms) #f))
                                   rst-terms)
-                            (append fst-vars rst-vars))]
+                            (append fst-vars
+                                    (if was-named-ellipsis? 
+                                        (list (id/depth (cadr terms) (length under) #f))
+                                        '())
+                                    rst-vars))]
                    [else
                     (define-values (fst-term fst-vars) 
                       (loop (car terms) under under-mismatch-ellipsis))
@@ -425,7 +438,7 @@
            (let ()
              (define final-match-repeat-name 
                (if (= 1 (hash-ref repeat-id-counts (syntax-e #'name)))
-                   #f
+                   (hash-ref original-repeat-names (syntax-e #'name) #f)
                    #'name))
              (define final-mismatch-repeat-name
                (if (and (syntax-e #'mismatch-name)
@@ -569,3 +582,13 @@
                            orig-stx)))
                       (not same-id?)))
                   (loop (cdr dups))))])))
+
+
+
+  (define (bind-pattern-names err-name names/ellipses vals body)
+    (with-syntax ([(names/ellipsis ...) names/ellipses]
+                  [(val ...) vals])
+      #`(term-let/error-name
+         #,err-name
+         ([names/ellipsis val] ...) 
+         #,body)))
\ No newline at end of file
diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/term.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/term.rkt
index 9f304b2791..442a5e2b8f 100644
--- a/pkgs/redex-pkgs/redex-lib/redex/private/term.rkt
+++ b/pkgs/redex-pkgs/redex-lib/redex/private/term.rkt
@@ -168,7 +168,9 @@
             (judgment-form-id? #'jf-name))
        (begin
          (unless (not (memq 'O (judgment-form-mode (syntax-local-value #'jf-name))))
-           (raise-syntax-error 'term "judgment forms with output mode (\"O\") positions disallowed" arg-stx stx))
+           (raise-syntax-error 'term 
+                               "judgment forms with output mode (\"O\") positions disallowed"
+                               arg-stx stx))
          (rewrite-application #'jf-name (syntax/loc stx (arg ...)) depth))]
       [f
        (and (identifier? (syntax f))
@@ -255,7 +257,9 @@
       (define m (regexp-match #rx"^([^_]*)_" (symbol->string id)))
       (when m
         (unless (memq (string->symbol (list-ref m 1)) (append pattern-symbols lang-nts))
-          (raise-syntax-error 'term "before underscore must be either a non-terminal or a built-in pattern" arg-stx stx)))))
+          (raise-syntax-error 'term 
+                              "before underscore must be either a non-terminal or a built-in pattern"
+                              arg-stx stx)))))
   
   (values
    (with-syntax ([rewritten (rewrite arg-stx)])
@@ -374,40 +378,46 @@
 (define-syntax (term-let/error-name stx)
   (syntax-case stx ()
     [(_ error-name ([x1 rhs1] [x rhs] ...) body1 body2 ...)
-     (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 (datum->syntax #'here (syntax-e #'x) #'x #'x)])
-                          (values (list #'x)
-                                  (list new-name)
-                                  (list depth)
-                                  new-name))]
-                       [(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)]))])
+     (let ()
+       (unless (identifier? #'error-name)
+         (raise-syntax-error 'term-let/error-name 
+                             "expected an identifier as the first argument"
+                             stx
+                             #'error-name))
+       (define-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 (datum->syntax #'here (syntax-e #'x) #'x #'x)])
+                (values (list #'x)
+                        (list new-name)
+                        (list depth)
+                        new-name))]
+             [(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)])))
        (with-syntax ([(orig-names ...) orig-names]
                      [(new-names ...) new-names]
                      [(depths ...) depths]
diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/rewrite-side-condition-test.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/rewrite-side-condition-test.rkt
index 5aeec908df..8849e83f28 100644
--- a/pkgs/redex-pkgs/redex-test/redex/tests/rewrite-side-condition-test.rkt
+++ b/pkgs/redex-pkgs/redex-test/redex/tests/rewrite-side-condition-test.rkt
@@ -24,8 +24,9 @@
 (check-equal? (rsc (1) () #t) `((list 1) () ()))
 (check-equal? (rsc (_ _ (name x _)) () #t) `((list any any (name x any)) (x) (x)))
 (check-equal? (rsc (1 ...) () #t) `((list (repeat 1 #f #f)) () ()))
-(check-equal? (rsc (1 ..._2) () #t) `((list (repeat 1 #f #f)) () ()))
-(check-equal? (rsc (1 ..._2 1 ..._2) () #t) `((list (repeat 1 ..._2 #f) (repeat 1 ..._2 #f)) () ()))
+(check-equal? (rsc (1 ..._2) () #t) `((list (repeat 1 ..._2 #f)) (..._2) (..._2)))
+(check-equal? (rsc (1 ..._2 1 ..._2) () #t) 
+              `((list (repeat 1 ..._2 #f) (repeat 1 ..._2 #f)) (..._2 ..._2) (..._2 ..._2)))
 (check-equal? (rsc (1 ..._!_3) () #t) `((list (repeat 1 #f #f)) () ()))
 (check-equal? (rsc (1 ..._!_3 1 ..._!_3) () #t)
               `((list (repeat 1 #f ..._!_3) (repeat 1 #f ..._!_3)) () ()))
@@ -42,7 +43,9 @@
               `((list (repeat (list (repeat (name x (nt x)) #f #f)) #f #f))
                 (x)
                 (((x ...) ...))))
-
+(check-equal? (rsc (any_1 any_1) (x) #f) `((list (name any_1 any) (name any_1 any)) 
+                                           (any_1 any_1) 
+                                           (any_1 any_1)))
 (check-equal? (rsc (in-hole (hole a #f (hide-hole hole)) (cross x)) '(x) #f)
               `((in-hole (list hole a #f (hide-hole hole)) (cross x-x))
                 ()