diff --git a/collects/redex/private/bitmap-test.ss b/collects/redex/private/bitmap-test.ss
index 7f92db36d4..5240b252cd 100644
--- a/collects/redex/private/bitmap-test.ss
+++ b/collects/redex/private/bitmap-test.ss
@@ -36,6 +36,20 @@
        (extend-reduction-relation red lang (--> 1 2)))
       "extended-reduction-relation.png")
 
+;; this test should fail because it gets the order wrong
+;; for the where/side-conditions
+(define red2
+  (reduction-relation
+   lang
+   (--> (number_a number_b number_c)
+        any_z
+        (where (any_x any_y) (number_a number_b))
+        (side-condition (= (term number_c) 5))
+        (where any_z any_x))))
+
+(test (render-reduction-relation red2)
+      "red2.png")
+        
 (define-metafunction lang
   [(S x v e) e])
 
@@ -92,7 +106,6 @@
         (render-metafunction Name))
       "metafunction-Name-vertical.png")
 
-
 ;; makes sure that there is no overlap inside or across metafunction calls  
 ;; or when there are unquotes involved
 (define-metafunction lang
diff --git a/collects/redex/private/bmps/metafunction-Name-vertical.png b/collects/redex/private/bmps/metafunction-Name-vertical.png
index cde38b7b0f..6d1d9f74ce 100644
Binary files a/collects/redex/private/bmps/metafunction-Name-vertical.png and b/collects/redex/private/bmps/metafunction-Name-vertical.png differ
diff --git a/collects/redex/private/pict.ss b/collects/redex/private/pict.ss
index edc56bbbfc..549e5e3c1c 100644
--- a/collects/redex/private/pict.ss
+++ b/collects/redex/private/pict.ss
@@ -251,7 +251,10 @@
            ltl-superimpose ltl-superimpose
            (list* 2 (+ 2 (current-label-extra-space))) 2)))
 
-(define (side-condition-pict fresh-vars side-conditions pattern-binds max-w)
+;; side-condition-pict : (listof pict) (listof (or/c (cons/c pict pict) pict)) number -> pict
+;; the elements of pattern-binds/sc that are pairs are bindings (ie "x = <something>")
+;;     and the elements of pattern-binds/sc that are just picts are just plain side-conditions
+(define (side-condition-pict fresh-vars pattern-binds/sc max-w)
   (let* ([frsh 
           (if (null? fresh-vars)
               null
@@ -264,16 +267,17 @@
                   fresh-vars))
                 (basic-text " fresh" (default-style)))))]
          [binds (map (lambda (b)
-                       (htl-append
-                        (car b)
-                        (make-=)
-                        (cdr b)))
-                     pattern-binds)]
+                       (if (pair? b)
+                           (htl-append
+                            (car b)
+                            (make-=)
+                            (cdr b))
+                           b))
+                     pattern-binds/sc)]
          [lst (add-between
                'comma
                (append
                 binds
-                side-conditions
                 frsh))])
     (if (null? lst)
         (blank)
@@ -293,8 +297,8 @@
 
 (define (rp->side-condition-pict rp max-w)
   (side-condition-pict (rule-pict-fresh-vars rp)
-                       (rule-pict-side-conditions rp)
-                       (rule-pict-pattern-binds rp)
+                       (append (rule-pict-side-conditions rp)
+                               (rule-pict-pattern-binds rp))
                        max-w))
 
 (define (rp->pict-label rp)
@@ -737,21 +741,21 @@
          [eqns (select-cases all-eqns)]
          [lhss (select-cases all-lhss)]
          [scs (map (lambda (eqn)
-                     (if (and (null? (list-ref eqn 1))
-                              (null? (list-ref eqn 2)))
+                     (if (null? (list-ref eqn 1))
                          #f
                          (side-condition-pict null 
-                                              (map wrapper->pict (list-ref eqn 1)) 
                                               (map (lambda (p)
-                                                     (cons (wrapper->pict (car p))
-                                                           (wrapper->pict (cdr p))))
-                                                   (list-ref eqn 2))
+                                                     (if (pair? p)
+                                                         (cons (wrapper->pict (car p))
+                                                               (wrapper->pict (cdr p)))
+                                                         (wrapper->pict p)))
+                                                   (list-ref eqn 1))
                                               (if (memq style '(up-down/vertical-side-conditions
                                                                 left-right/vertical-side-conditions))
                                                   0
                                                   +inf.0))))
                    eqns)]
-         [rhss (map (lambda (eqn) (wrapper->pict (list-ref eqn 3))) eqns)]
+         [rhss (map (lambda (eqn) (wrapper->pict (list-ref eqn 2))) eqns)]
          [linebreak-list (or current-linebreaks
                              (map (lambda (x) #f) eqns))]
          [=-pict (make-=)]
diff --git a/collects/redex/private/reduction-semantics.ss b/collects/redex/private/reduction-semantics.ss
index ed3744370d..f0ae73e8d7 100644
--- a/collects/redex/private/reduction-semantics.ss
+++ b/collects/redex/private/reduction-semantics.ss
@@ -1074,177 +1074,180 @@
            (raise-syntax-error syn-error-name "no clauses" orig-stx))
          (prune-syntax
           (let ([lang-nts (language-id-nts #'lang 'define-metafunction)])  ;; keep this near the beginning, so it signals the first error (PR 10062)
-            (let-values ([(contract-name dom-ctcs codom-contract pats)
-                          (split-out-contract orig-stx syn-error-name #'rest relation?)])
-              (with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats]
-                            [(lhs-for-lw ...)
-                             (with-syntax ([((lhs-for-lw _ ...) ...) pats])
-                               (map (λ (x) (to-lw/proc (datum->syntax #f (cdr (syntax-e x)) x)))
-                                    (syntax->list #'(lhs-for-lw ...))))])
-                (with-syntax ([((rhs stuff ...) ...) (if relation?
-                                                         #'((,(and (term raw-rhses) ...)) ...)
-                                                         #'((raw-rhses ...) ...))])
-                  (parameterize ([is-term-fn? 
-                                  (let ([names (syntax->list #'(original-names ...))])
-                                    (λ (x) (and (not (null? names))
-                                                (identifier? (car names))
-                                                (free-identifier=? x (car names)))))])
-                    (with-syntax ([(rhs/lw ...) (map to-lw/proc (syntax->list #'(rhs ...)))]
-                                  [(lhs ...) #'((lhs-clauses ...) ...)]
-                                  [name (let loop ([name (if contract-name
-                                                             contract-name
-                                                             (car (syntax->list #'(original-names ...))))]
-                                                   [names (if contract-name
-                                                              (syntax->list #'(original-names ...))
-                                                              (cdr (syntax->list #'(original-names ...))))])
-                                          (cond
-                                            [(null? names) name]
-                                            [else
-                                             (unless (eq? (syntax-e name) (syntax-e (car names)))
-                                               (raise
-                                                (make-exn:fail:syntax
-                                                 (if contract-name
-                                                     "define-metafunction: expected each clause and the contract to use the same name"
-                                                     "define-metafunction: expected each clause to use the same name")
-                                                 (current-continuation-marks)
-                                                 (list name
-                                                       (car names)))))
-                                             (loop name (cdr names))]))])
-                      
-                      (with-syntax ([(((tl-side-conds ...) ...) 
-                                      (tl-bindings ...)
-                                      (tl-side-cond/binds ...))
-                                     (parse-extras #'((stuff ...) ...))])
-                        (with-syntax ([(((cp-let-bindings ...) rhs/wheres) ...)
-                                       (map (λ (sc/b rhs) 
-                                              (let-values ([(body-code cp-let-bindings) 
-                                                            (bind-withs
-                                                             syn-error-name '()  
-                                                             #'lang lang-nts
-                                                             sc/b 'flatten
-                                                             #`(list (term #,rhs)))])
-                                                (list cp-let-bindings body-code)))
-                                            (syntax->list #'(tl-side-cond/binds ...))
-                                            (syntax->list #'(rhs ...)))]
-                                      [(((rg-cp-let-bindings ...) rg-rhs/wheres) ...)
-                                       (map (λ (sc/b rhs) 
-                                              (let-values ([(body-code cp-let-bindings) 
-                                                            (bind-withs
-                                                             syn-error-name '()  
-                                                             #'lang lang-nts
-                                                             sc/b 'predicate
-                                                             #`#t)])
-                                                (list cp-let-bindings body-code)))
-                                            (syntax->list #'(tl-side-cond/binds ...))
+          (let-values ([(contract-name dom-ctcs codom-contract pats)
+                        (split-out-contract orig-stx syn-error-name #'rest relation?)])
+            (with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats]
+                          [(lhs-for-lw ...)
+                           (with-syntax ([((lhs-for-lw _ ...) ...) pats])
+                             (map (λ (x) (to-lw/proc (datum->syntax #f (cdr (syntax-e x)) x)))
+                                  (syntax->list #'(lhs-for-lw ...))))])
+              (with-syntax ([((rhs stuff ...) ...) (if relation?
+                                                       #'((,(and (term raw-rhses) ...)) ...)
+                                                       #'((raw-rhses ...) ...))])
+              (parameterize ([is-term-fn? 
+                              (let ([names (syntax->list #'(original-names ...))])
+                                (λ (x) (and (not (null? names))
+                                            (identifier? (car names))
+                                            (free-identifier=? x (car names)))))])
+                (with-syntax ([(rhs/lw ...) (map to-lw/proc (syntax->list #'(rhs ...)))]
+                              [(lhs ...) #'((lhs-clauses ...) ...)]
+                              [name (let loop ([name (if contract-name
+                                                         contract-name
+                                                         (car (syntax->list #'(original-names ...))))]
+                                               [names (if contract-name
+                                                          (syntax->list #'(original-names ...))
+                                                          (cdr (syntax->list #'(original-names ...))))])
+                                      (cond
+                                        [(null? names) name]
+                                        [else
+                                         (unless (eq? (syntax-e name) (syntax-e (car names)))
+                                           (raise
+                                            (make-exn:fail:syntax
+                                             (if contract-name
+                                                 "define-metafunction: expected each clause and the contract to use the same name"
+                                                 "define-metafunction: expected each clause to use the same name")
+                                             (current-continuation-marks)
+                                             (list name
+                                                   (car names)))))
+                                         (loop name (cdr names))]))])
+                  
+                  (with-syntax ([(((tl-side-conds ...) ...) 
+                                  (tl-bindings ...)
+                                  (tl-side-cond/binds ...))
+                                 (parse-extras #'((stuff ...) ...))])
+                      (with-syntax ([(((cp-let-bindings ...) rhs/wheres) ...)
+                                     (map (λ (sc/b rhs) 
+                                            (let-values ([(body-code cp-let-bindings) 
+                                                          (bind-withs
+                                                           syn-error-name '()  
+                                                           #'lang lang-nts
+                                                           sc/b 'flatten
+                                                           #`(list (term #,rhs)))])
+                                              (list cp-let-bindings body-code)))
+                                          (syntax->list #'(tl-side-cond/binds ...))
+                                          (syntax->list #'(rhs ...)))]
+                                    [(((rg-cp-let-bindings ...) rg-rhs/wheres) ...)
+                                     (map (λ (sc/b rhs) 
+                                            (let-values ([(body-code cp-let-bindings) 
+                                                          (bind-withs
+                                                           syn-error-name '()  
+                                                           #'lang lang-nts
+                                                           sc/b 'predicate
+                                                           #`#t)])
+                                              (list cp-let-bindings body-code)))
+                                          (syntax->list #'(tl-side-cond/binds ...))
+                                          (syntax->list #'(rhs ...)))])
+                        (with-syntax ([(side-conditions-rewritten ...) 
+                                       (map (λ (x) (rewrite-side-conditions/check-errs
+                                                    lang-nts
+                                                    syn-error-name
+                                                    #t
+                                                    x))
+                                            (syntax->list (syntax (lhs ...))))]
+                                      [(rg-side-conditions-rewritten ...) 
+                                       (map (λ (x) (rewrite-side-conditions/check-errs
+                                                    lang-nts
+                                                    syn-error-name
+                                                    #t
+                                                    x))
+                                            (syntax->list (syntax ((side-condition lhs rg-rhs/wheres) ...))))]
+                                      [dom-side-conditions-rewritten
+                                       (and dom-ctcs
+                                            (rewrite-side-conditions/check-errs
+                                             lang-nts
+                                             syn-error-name
+                                             #f
+                                             dom-ctcs))]
+                                      [codom-side-conditions-rewritten
+                                       (rewrite-side-conditions/check-errs
+                                        lang-nts
+                                        syn-error-name
+                                        #f
+                                        codom-contract)]
+                                      [(rhs-fns ...)
+                                       (map (λ (lhs rhs/where)
+                                              (let-values ([(names names/ellipses) 
+                                                            (extract-names lang-nts syn-error-name #t lhs)])
+                                                (with-syntax ([(names ...) names]
+                                                              [(names/ellipses ...) names/ellipses]
+                                                              [rhs/where rhs/where])
+                                                  (syntax
+                                                   (λ (name bindings)
+                                                     (term-let-fn ((name name))
+                                                                  (term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
+                                                                            rhs/where)))))))
+                                            (syntax->list (syntax (lhs ...)))
+                                            (syntax->list (syntax (rhs/wheres ...))))]
+                                      [(name2 name-predicate) (generate-temporaries (syntax (name name)))]
+                                      [(((bind-id/lw . bind-pat/lw) ...) ...)
+                                       ;; Also for pict, extract pattern bindings
+                                       (map (λ (x) (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/proc (cdr x))))
+                                                        (extract-pattern-binds x)))
+                                            (syntax->list #'(lhs ...)))]
+                                      
+                                      
+                                      [((where/sc/lw ...) ...)
+                                       ;; Also for pict, extract where bindings
+                                       (map (λ (hm)
+                                              (map
+                                               (λ (lst)
+                                                 (syntax-case lst (side-condition where)
+                                                   [(where pat exp)
+                                                    #`(cons #,(to-lw/proc #'pat) #,(to-lw/proc #'exp))]
+                                                   [(side-condition x)
+                                                    (to-lw/uq/proc #'x)]))
+                                               (syntax->list hm)))
+                                            (syntax->list #'(tl-side-cond/binds ...)))]
+                                      
+                                      [(((rhs-bind-id/lw . rhs-bind-pat/lw/uq) ...) ...)
+                                       ;; Also for pict, extract pattern bindings
+                                       (map (λ (x) (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/uq/proc (cdr x))))
+                                                        (extract-term-let-binds x)))
                                             (syntax->list #'(rhs ...)))])
-                          (with-syntax ([(side-conditions-rewritten ...) 
-                                         (map (λ (x) (rewrite-side-conditions/check-errs
-                                                      lang-nts
-                                                      syn-error-name
-                                                      #t
-                                                      x))
-                                              (syntax->list (syntax (lhs ...))))]
-                                        [(rg-side-conditions-rewritten ...) 
-                                         (map (λ (x) (rewrite-side-conditions/check-errs
-                                                      lang-nts
-                                                      syn-error-name
-                                                      #t
-                                                      x))
-                                              (syntax->list (syntax ((side-condition lhs rg-rhs/wheres) ...))))]
-                                        [dom-side-conditions-rewritten
-                                         (and dom-ctcs
-                                              (rewrite-side-conditions/check-errs
-                                               lang-nts
-                                               syn-error-name
-                                               #f
-                                               dom-ctcs))]
-                                        [codom-side-conditions-rewritten
-                                         (rewrite-side-conditions/check-errs
-                                          lang-nts
-                                          syn-error-name
-                                          #f
-                                          codom-contract)]
-                                        [(rhs-fns ...)
-                                         (map (λ (lhs rhs/where bindings)
-                                                (let-values ([(names names/ellipses) 
-                                                              (extract-names lang-nts syn-error-name #t lhs)])
-                                                  (with-syntax ([(names ...) names]
-                                                                [(names/ellipses ...) names/ellipses]
-                                                                [rhs/where rhs/where]
-                                                                [((tl-var tl-exp) ...) bindings])
-                                                    (syntax 
-                                                     (λ (name bindings)
-                                                       (term-let-fn ((name name))
-                                                                    (term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
-                                                                              (term-let ([tl-var (term tl-exp)] ...)
-                                                                                        rhs/where))))))))
-                                              (syntax->list (syntax (lhs ...)))
-                                              (syntax->list (syntax (rhs/wheres ...)))
-                                              (syntax->list (syntax (tl-bindings ...))))]
-                                        [(name2 name-predicate) (generate-temporaries (syntax (name name)))]
-                                        [((side-cond/lw/uq ...) ...)
-                                         (map (lambda (scs) (map to-lw/uq/proc (syntax->list scs)))
-                                              (syntax->list #'((tl-side-conds ...) ...)))]
-                                        [(((bind-id/lw . bind-pat/lw) ...) ...)
-                                         ;; Also for pict, extract pattern bindings
-                                         (map (λ (x) (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/proc (cdr x))))
-                                                          (extract-pattern-binds x)))
-                                              (syntax->list #'(lhs ...)))]
-                                        [(((rhs-bind-id/lw . rhs-bind-pat/lw/uq) ...) ...)
-                                         ;; Also for pict, extract pattern bindings
-                                         (map (λ (x) (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/uq/proc (cdr x))))
-                                                          (extract-term-let-binds x)))
-                                              (syntax->list #'(rhs ...)))]
-                                        [(((where-id/lw where-pat/lw) ...) ...)
-                                         ;; Also for pict, extract where bindings
-                                         (map (λ (lst) (map (λ (ab) (map to-lw/proc (syntax->list ab)))
-                                                            (syntax->list lst)))
-                                              (syntax->list #'(tl-bindings ...)))])
-                            (syntax-property
-                             #`(begin
-                                 (define-values (name2 name-predicate)
-                                   (let ([sc `(side-conditions-rewritten ...)]
-                                         [dsc `dom-side-conditions-rewritten]
-                                         cp-let-bindings ... ...
-                                         rg-cp-let-bindings ... ...)
-                                     (let ([rg-sc `(rg-side-conditions-rewritten ...)])
-                                       (build-metafunction 
-                                        lang
-                                        sc
-                                        (list rhs-fns ...)
-                                        #,(if prev-metafunction
-                                              (let ([term-fn (syntax-local-value prev-metafunction)])
-                                                #`(metafunc-proc-cps #,(term-fn-get-id term-fn)))
-                                              #''())
-                                        #,(if prev-metafunction
-                                              (let ([term-fn (syntax-local-value prev-metafunction)])
-                                                #`(metafunc-proc-rhss #,(term-fn-get-id term-fn)))
-                                              #''())
-                                        (λ (f/dom cps rhss)
-                                          (make-metafunc-proc
-                                           (let ([name (lambda (x) (f/dom x))]) name)
-                                           (list (list lhs-for-lw
-                                                       (list side-cond/lw/uq ...)
-                                                       (list (cons bind-id/lw bind-pat/lw) ...
-                                                             (cons rhs-bind-id/lw rhs-bind-pat/lw/uq) ...
-                                                             (cons where-id/lw where-pat/lw) ...)
-                                                       rhs/lw)
-                                                 ...)
-                                           lang
-                                           #t ;; multi-args?
-                                           'name
-                                           cps
-                                           rhss
-                                           (let ([name (lambda (x) (name-predicate x))]) name)
-                                           dsc
-                                           rg-sc))
-                                        dsc
-                                        `codom-side-conditions-rewritten
-                                        'name
-                                        #,relation?))))
-                                 (term-define-fn name name2))
-                             'disappeared-use
-                             (map syntax-local-introduce (syntax->list #'(original-names ...)))))))))))))))]
+                          (syntax-property
+                           #`(begin
+                               (define-values (name2 name-predicate)
+                                 (let ([sc `(side-conditions-rewritten ...)]
+                                       [dsc `dom-side-conditions-rewritten]
+                                       cp-let-bindings ... ...
+                                       rg-cp-let-bindings ... ...)
+                                   (let ([rg-sc `(rg-side-conditions-rewritten ...)])
+                                     (build-metafunction 
+                                      lang
+                                      sc
+                                      (list rhs-fns ...)
+                                      #,(if prev-metafunction
+                                            (let ([term-fn (syntax-local-value prev-metafunction)])
+                                              #`(metafunc-proc-cps #,(term-fn-get-id term-fn)))
+                                            #''())
+                                      #,(if prev-metafunction
+                                            (let ([term-fn (syntax-local-value prev-metafunction)])
+                                              #`(metafunc-proc-rhss #,(term-fn-get-id term-fn)))
+                                            #''())
+                                      (λ (f/dom cps rhss)
+                                        (make-metafunc-proc
+                                         (let ([name (lambda (x) (f/dom x))]) name)
+                                         (list (list lhs-for-lw
+                                                     (list (cons bind-id/lw bind-pat/lw) ...
+                                                           (cons rhs-bind-id/lw rhs-bind-pat/lw/uq) ...
+                                                           where/sc/lw ...)
+                                                     rhs/lw)
+                                               ...)
+                                         lang
+                                         #t ;; multi-args?
+                                         'name
+                                         cps
+                                         rhss
+                                         (let ([name (lambda (x) (name-predicate x))]) name)
+                                         dsc
+                                         rg-sc))
+                                      dsc
+                                      `codom-side-conditions-rewritten
+                                      'name
+                                      #,relation?))))
+                               (term-define-fn name name2))
+                           'disappeared-use
+                           (map syntax-local-introduce (syntax->list #'(original-names ...)))))))))))))))]
       [(_ prev-metafunction name lang clauses ...)
        (begin
          (unless (identifier? #'name)
@@ -1430,7 +1433,7 @@
                                         (redex-error name "~a matched ~s ~a different ways and returned different results" 
                                                      (if (< num 0)
                                                          "a clause from an extended metafunction"
-                                                         (format "clause ~a" num))
+                                                         (format "clause #~a (counting from 0)" num))
                                                      `(,name ,@exp)
                                                      (length mtchs))]
                                        [else
diff --git a/collects/redex/private/struct.ss b/collects/redex/private/struct.ss
index 0627ffa9c3..d080348826 100644
--- a/collects/redex/private/struct.ss
+++ b/collects/redex/private/struct.ss
@@ -50,27 +50,37 @@
 ;; I started to add it, but didn't finish. -robby
 (define (build-reduction-relation orig-reduction-relation lang make-procs rule-names lws domain-pattern)
   (let* ([make-procs/check-domain
-          (map (λ (make-proc)
-                 (make-rewrite-proc
-                  (λ (lang)
-                    (let ([compiled-domain-pat (compile-pattern lang domain-pattern #f)]
-                          [proc (make-proc lang)])
-                      (λ (tl-exp exp f acc)
-                        (unless (match-pattern compiled-domain-pat tl-exp)
-                          (error 'reduction-relation "relation not defined for ~s" tl-exp))
-                        (let ([ress (proc tl-exp exp f acc)])
-                          (for-each
-                           (λ (res)
-                             (let ([term (cadr res)])
-                               (unless (match-pattern compiled-domain-pat term)
-                                 (error 'reduction-relation "relation reduced to ~s, which is outside its domain"
-                                        term))))
-                           ress)
-                          ress))))
-                  (rewrite-proc-name make-proc)
-                  (rewrite-proc-lhs make-proc)
-                  (rewrite-proc-id make-proc)))
-               make-procs)])
+          (let loop ([make-procs make-procs]
+                     [i 0])
+            (cond
+              [(null? make-procs) null]
+              [else
+               (let ([make-proc (car make-procs)])
+                 (cons (make-rewrite-proc
+                        (λ (lang)
+                          (let ([compiled-domain-pat (compile-pattern lang domain-pattern #f)]
+                                [proc (make-proc lang)])
+                            (λ (tl-exp exp f acc)
+                              (unless (match-pattern compiled-domain-pat tl-exp)
+                                (error 'reduction-relation "relation not defined for ~s" tl-exp))
+                              (let ([ress (proc tl-exp exp f acc)])
+                                (for-each
+                                 (λ (res)
+                                   (let ([term (cadr res)])
+                                     (unless (match-pattern compiled-domain-pat term)
+                                       (error 'reduction-relation "relation reduced to ~s via ~a, which is outside its domain"
+                                              term
+                                              (let ([name (rewrite-proc-name make-proc)])
+                                                (if name
+                                                    (format "the rule named ~a" name)
+                                                    (format "rule #~a (counting from 0)" i)))))))
+                                 ress)
+                                ress))))
+                        (rewrite-proc-name make-proc)
+                        (rewrite-proc-lhs make-proc)
+                        (rewrite-proc-id make-proc))
+                       (loop (cdr make-procs)
+                             (+ i 1))))]))])
     (cond
       [orig-reduction-relation
        (let* ([new-names (map rewrite-proc-name make-procs)]
diff --git a/collects/redex/private/tl-test.ss b/collects/redex/private/tl-test.ss
index f03ef20d4c..e52093a7f8 100644
--- a/collects/redex/private/tl-test.ss
+++ b/collects/redex/private/tl-test.ss
@@ -639,14 +639,25 @@
     
     (test (term (f 1 1 1 1 1)) (term 1)))
   
-   (let ()
-     (define-metafunction empty-language
-       [(ex variable_x) 
-        variable_x
-        (where quote variable_x)])
-
-     (test (term (ex quote)) (term quote)))
+  (let ()
+    (define-metafunction empty-language
+      [(ex variable_x) 
+       variable_x
+       (where quote variable_x)])
+    
+    (test (term (ex quote)) (term quote)))
   
+  (let ()
+    (define-metafunction empty-language
+      [(f any ...)
+       (any ...)
+       (where variable_1 x)
+       (side-condition #f)
+       (where (number ...) y)]
+      [(f any ...)
+       12345])
+    
+    (test (term (f 8)) 12345))
   
   
 ;                                                                                                 
@@ -924,7 +935,7 @@
           (with-handlers ((exn? exn-message))
             (apply-reduction-relation red 1)
             'no-exception-raised))
-        "reduction-relation: relation reduced to x, which is outside its domain")
+        "reduction-relation: relation reduced to x via rule #0 (counting from 0), which is outside its domain")
 
   (let* ([red1
           (reduction-relation