diff --git a/collects/redex/private/reduction-semantics.ss b/collects/redex/private/reduction-semantics.ss
index b57539df09..db9c0c8562 100644
--- a/collects/redex/private/reduction-semantics.ss
+++ b/collects/redex/private/reduction-semantics.ss
@@ -11,8 +11,10 @@
 (require (for-syntax (lib "name.ss" "syntax")
                      "rewrite-side-conditions.ss"
                      "term-fn.ss"
+                     "underscore-allowed.ss"
                      (lib "boundmap.ss" "syntax")
-                     scheme/base))
+                     scheme/base
+                     (prefix-in pattern- scheme/match)))
 
 (define (language-nts lang)
   (hash-map (compiled-lang-ht lang) (λ (x y) x)))
@@ -440,16 +442,17 @@
                       (syntax->list (syntax (extras ...)))
                       lang-id))]
       [((rhs-arrow rhs-from rhs-to) (lhs-arrow lhs-frm-id lhs-to-id))
-       (let ([lang-nts (language-id-nts lang-id orig-name)])
+       (let* ([lang-nts (language-id-nts lang-id orig-name)]
+              [rewrite-side-conds
+               (λ (pat) (rewrite-side-conditions/check-errs lang-nts orig-name #t pat))])
          (let-values ([(names names/ellipses) (extract-names lang-nts orig-name #t (syntax rhs-from))])
            (with-syntax ([(names ...) names]
                          [(names/ellipses ...) names/ellipses]
-                         [side-conditions-rewritten (rewrite-side-conditions/check-errs
-                                                     lang-nts
-                                                     orig-name
-                                                     #t
+                         [side-conditions-rewritten (rewrite-side-conds
                                                      (rewrite-node-pat (syntax-e (syntax lhs-frm-id))
-                                                                       (syntax->datum (syntax rhs-from))))]
+                                                                       (syntax rhs-from)))]
+                         [fresh-rhs-from (rewrite-side-conds 
+                                          (freshen-names #'rhs-from #'lhs-frm-id lang-nts orig-name))]
                          [lang lang])
              (map
               (λ (child-proc)
@@ -460,19 +463,51 @@
                    (λ (bindings rhs-binder)
                      (term-let ([lhs-to-id rhs-binder]
                                 [names/ellipses (lookup-binding bindings 'names)] ...)
-                       (term rhs-to)))
-                   #,child-proc))
+                               (term rhs-to)))
+                   #,child-proc
+                   `fresh-rhs-from))
               (get-choices stx orig-name bm #'lang
                            (syntax lhs-arrow) 
                            name-table lang-id 
-                           allow-zero-rules?)))))]))  
+                           allow-zero-rules?)))))]))
   (define (rewrite-node-pat id term)
-    (let loop ([term term])
-      (cond
-        [(eq? id term) `(name ,id any)]
-        [(pair? term) (cons (loop (car term))
-                            (loop (cdr term)))]
-        [else term])))
+    (let loop ([t term])
+      (syntax-case t (side-condition)
+        [(side-condition p c)
+         #`(side-condition #,(loop #'p) c)]
+        [(p ...)
+         (map loop (syntax->list #'(p ...)))]
+        [else 
+         (if (and (identifier? t) (eq? id (syntax-e t)))
+             `(name ,id any)
+             t)])))
+  
+  (define (freshen-names pat hole-id nts what)
+    (define (fresh x)
+      (gensym
+       (if (or (memq x nts) (memq x underscore-allowed))
+           (string-append (symbol->string x) "_")
+           x)))
+    (let-values ([(bound _) (extract-names nts what #t pat #f)])
+      (let ([renames (make-bound-identifier-mapping)])
+        (for-each 
+         (λ (x)
+           (unless (bound-identifier=? x hole-id)
+             (bound-identifier-mapping-put! renames x (fresh (syntax-e x)))))
+         bound)
+        (let recur ([p pat])
+          (syntax-case p (side-condition)
+            [(side-condition p c)
+             #`(side-condition 
+                #,(recur #'p)
+                (term-let (#,@(bound-identifier-mapping-map renames (λ (x y) #`(#,x (term #,y)))))
+                          c))]
+            [(p ...)
+             #`(#,@(map recur (syntax->list #'(p ...))))]
+            [else
+             (if (identifier? p)
+                 (bound-identifier-mapping-get renames p (λ () p))
+                 p)])))))
   
   (define (do-leaf stx orig-name lang name-table from to extras lang-id)
     (let ([lang-nts (language-id-nts lang-id orig-name)])
@@ -484,7 +519,7 @@
                           orig-name
                           #t
                           from)]
-                        [to to]
+                        [to to #;#`,(begin (printf "~s\n" #,name) (term #,to))]
                         [name name]
                         [lang lang]
                         [(names ...) names]
@@ -639,6 +674,18 @@
           (cons (format " ~s" (syntax->datum (car stxs)))
                 (loop (cdr stxs)))])))))
 
+(define (substitute from to pat)
+  (let recur ([p pat])
+    (syntax-case p (side-condition)
+      [(side-condition p c)
+       #`(side-condition #,(recur #'p) c)]
+      [(p ...)
+       #`(#,@(map recur (syntax->list #'(p ...))))]
+      [else
+       (if (and (identifier? p) (bound-identifier=? p from))
+           to
+           p)])))
+
 (define (verify-name-ok orig-name the-name)
   (unless (symbol? the-name)
     (error orig-name "expected a single name, got ~s" the-name)))
@@ -679,7 +726,12 @@
      (apply append (map reduction-relation-lws lst))
      `any)))
 
-(define (do-node-match lhs-frm-id lhs-to-id pat rhs-proc child-make-proc)
+(define (do-node-match lhs-frm-id lhs-to-id pat rhs-proc child-make-proc rhs-from)
+  (define (subst from to in)
+    (let recur ([p in])
+      (cond [(eq? from p) to]
+            [(pair? p) (map recur p)]
+            [else p])))
   ;; need call to make-rewrite-proc
   ;; also need a test case here to check duplication of names.
   (make-rewrite-proc
@@ -701,7 +753,8 @@
                                           (λ (x) (f (rhs-proc (mtch-bindings (car mtchs)) x)))
                                           acc)))]))
                other-matches)))))
-   (rewrite-proc-name child-make-proc)))
+   (rewrite-proc-name child-make-proc)
+   (subst lhs-frm-id (rewrite-proc-lhs child-make-proc) rhs-from)))
 
 (define (do-leaf-match name pat proc)
   (make-rewrite-proc
@@ -717,7 +770,8 @@
                        mtchs
                        other-matches)
                other-matches)))))
-   name))
+   name
+   pat))
 
 (define-syntax (test-match stx)
   (syntax-case stx ()
@@ -758,7 +812,7 @@
                           (symbol->string (bind-name y))))))
 
 (define-values (struct:metafunc-proc make-metafunc-proc metafunc-proc? metafunc-proc-ref metafunc-proc-set!)
-  (make-struct-type 'metafunc-proc #f 9 0 #f null (current-inspector) 0))
+  (make-struct-type 'metafunc-proc #f 10 0 #f null (current-inspector) 0))
 (define metafunc-proc-pict-info (make-struct-field-accessor metafunc-proc-ref 1))
 (define metafunc-proc-lang (make-struct-field-accessor metafunc-proc-ref 2))
 (define metafunc-proc-multi-arg? (make-struct-field-accessor metafunc-proc-ref 3))
@@ -767,6 +821,7 @@
 (define metafunc-proc-rhss (make-struct-field-accessor metafunc-proc-ref 6))
 (define metafunc-proc-in-dom? (make-struct-field-accessor metafunc-proc-ref 7))
 (define metafunc-proc-dom-pat (make-struct-field-accessor metafunc-proc-ref 8))
+(define metafunc-proc-lhs-pats (make-struct-field-accessor metafunc-proc-ref 9))
 (define-struct metafunction (proc))
 
 (define-syntax (in-domain? stx)
@@ -937,7 +992,8 @@
                                cps
                                rhss
                                (let ([name (lambda (x) (name-predicate x))]) name)
-                               `dom-side-conditions-rewritten))
+                               `dom-side-conditions-rewritten
+                               `(side-conditions-rewritten ...)))
                             `dom-side-conditions-rewritten
                             `codom-side-conditions-rewritten
                             'name))
@@ -1714,6 +1770,7 @@
          metafunc-proc-rhss
          metafunc-proc-in-dom?
          metafunc-proc-dom-pat
+         metafunc-proc-lhs-pats
          
          (struct-out binds))
 
diff --git a/collects/redex/private/rewrite-side-conditions.ss b/collects/redex/private/rewrite-side-conditions.ss
index 8086c8725b..398b29f1f8 100644
--- a/collects/redex/private/rewrite-side-conditions.ss
+++ b/collects/redex/private/rewrite-side-conditions.ss
@@ -1,9 +1,10 @@
-(module rewrite-side-conditions mzscheme
+(module rewrite-side-conditions scheme/base
   (require (lib "list.ss")
            "underscore-allowed.ss")
-  (require-for-template mzscheme
-                        "term.ss"
-                        "matcher.ss")
+  (require (for-template
+            mzscheme
+            "term.ss"
+            "matcher.ss"))
   
   (provide rewrite-side-conditions/check-errs
            extract-names
@@ -85,7 +86,7 @@
   (define-struct id/depth (id depth))
   
   ;; extract-names : syntax syntax -> (values (listof syntax) (listof syntax[x | (x ...) | ((x ...) ...) | ...]))
-  (define (extract-names all-nts what bind-names? orig-stx)
+  (define (extract-names all-nts what bind-names? orig-stx [rhs-only? #t])
     (let* ([dups
             (let loop ([stx orig-stx]
                        [names null]
@@ -115,8 +116,8 @@
                      [else 
                       (if (or (null? (cdr pats))
                               (not (identifier? (cadr pats)))
-                              (not (or (module-identifier=? (quote-syntax ...)
-                                                            (cadr pats))
+                              (not (or (free-identifier=? (quote-syntax ...)
+                                                          (cadr pats))
                                        (let ([inside (syntax-e (cadr pats))])
                                          (regexp-match #rx"^\\.\\.\\._" (symbol->string inside))))))
                           (i-loop (cdr pats)
@@ -125,7 +126,8 @@
                                   (loop (car pats) names (+ depth 1))))]))]
                 [x
                  (and (identifier? (syntax x))
-                      (binds-in-right-hand-side? all-nts bind-names? (syntax x)))
+                      ((if rhs-only? binds-in-right-hand-side? binds?)
+                       all-nts bind-names? (syntax x)))
                  (cons (make-id/depth (syntax x) depth) names)]
                 [else names]))]
            [no-dups (filter-duplicates what orig-stx dups)])
@@ -141,14 +143,16 @@
                             [dots (quote-syntax ...)])
                 (syntax (rest dots)))])))
   
-  
-  (define (binds-in-right-hand-side? nts bind-names? x)
+  (define (binds? nts bind-names? x)
     (or (and bind-names? (memq (syntax-e x) nts))
         (and bind-names? (memq (syntax-e x) underscore-allowed))
-        (let ([str (symbol->string (syntax-e x))])
-          (and (regexp-match #rx"_" str)
-               (not (regexp-match #rx"^\\.\\.\\._" str))
-               (not (regexp-match #rx"_!_" str))))))
+        (regexp-match #rx"_" (symbol->string (syntax-e x)))))
+  
+  (define (binds-in-right-hand-side? nts bind-names? x)
+    (and (binds? nts bind-names? x)
+         (let ([str (symbol->string (syntax-e x))])
+           (and (not (regexp-match #rx"^\\.\\.\\._" str))
+                (not (regexp-match #rx"_!_" str))))))
   
   (define (filter-duplicates what orig-stx dups)
     (let loop ([dups dups])
@@ -158,8 +162,8 @@
          (cons
           (car dups)
           (filter (lambda (x) 
-                    (let ([same-id? (module-identifier=? (id/depth-id x)
-                                                         (id/depth-id (car dups)))])
+                    (let ([same-id? (free-identifier=? (id/depth-id x)
+                                                       (id/depth-id (car dups)))])
                       (when same-id?
                         (unless (equal? (id/depth-depth x)
                                         (id/depth-depth (car dups)))
@@ -167,7 +171,7 @@
                            (make-exn:fail:syntax
                             (format "~a: found the same binder, ~s, at different depths, ~a and ~a"
                                     what
-                                    (syntax-object->datum (id/depth-id x))
+                                    (syntax->datum (id/depth-id x))
                                     (id/depth-depth x)
                                     (id/depth-depth (car dups)))
                             (current-continuation-marks)
diff --git a/collects/redex/private/rg-test.ss b/collects/redex/private/rg-test.ss
index 836183f185..299eb3aa06 100644
--- a/collects/redex/private/rg-test.ss
+++ b/collects/redex/private/rg-test.ss
@@ -90,6 +90,21 @@
   (test (pick-char 0 null (make-random 65)) #\a)
   (test (random-string null null 1 0 (make-random 65)) "a"))
 
+(let ()
+  (define-language L
+    (a 5 (x a) #:binds x a)
+    (b 4))
+  (test ((pick-nt 'dontcare) 'a L '(x) 1)
+        (nt-rhs (car (compiled-lang-lang L))))
+  (test ((pick-nt 'dontcare (make-random 1)) 'a L '(x) preferred-production-threshold)
+        (nt-rhs (car (compiled-lang-lang L))))
+  (let ([pref (car (nt-rhs (car (compiled-lang-lang L))))])
+    (test ((pick-nt (make-immutable-hash `((a ,pref))) (make-random 0))
+           'a L '(x) preferred-production-threshold)
+          (list pref)))
+  (test ((pick-nt 'dontcare) 'sexp sexp null preferred-production-threshold)
+        (nt-rhs (car (compiled-lang-lang sexp)))))
+
 (define-syntax exn:fail-message
   (syntax-rules ()
     [(_ expr)
@@ -101,7 +116,9 @@
            (make-exn-not-raised))))]))
 
 (define (patterns . selectors) 
-  (map (λ (selector) (λ (name prods vars size) (list (selector prods))))
+  (map (λ (selector) 
+         (λ (name lang vars size)
+           (list (selector (nt-rhs (nt-by-name lang name))))))
        selectors))
 
 (define (iterator name items)
@@ -145,7 +162,7 @@
   
   ;; Generate (λ (x) x)
   (test 
-   (generate/decisions 
+   (generate-term 
     lc e 1 0
     (decisions #:var (list (λ _ 'x) (λ _'x))
                #:nt (patterns third first first first)))
@@ -153,14 +170,14 @@
   
   ;; Generate pattern that's not a non-terminal
   (test 
-   (generate/decisions 
+   (generate-term 
     lc (x x x_1 x_1) 1 0
     (decisions #:var (list (λ _ 'x) (λ _ 'y)))) 
    '(x x y y))
   
   ; After choosing (e e), size decremented forces each e to x.
   (test
-   (generate/decisions 
+   (generate-term 
     lc e 1 0
     (decisions #:nt (patterns first)
                #:var (list (λ _ 'x) (λ _ 'y))))
@@ -176,7 +193,7 @@
   (let* ([x null]
          [prepend! (λ (c l b a) (begin (set! x (cons (car b) x)) 'x))])
     (test (begin
-            (generate/decisions lang a 5 0 (decisions #:var (list (λ _ 'x) prepend! prepend!)))
+            (generate-term lang a 5 0 (decisions #:var (list (λ _ 'x) prepend! prepend!)))
             x)
           '(x x))))
 
@@ -187,7 +204,7 @@
     (x (variable-except λ)))
   (test 
    (exn:fail-message 
-     (generate/decisions 
+     (generate-term 
       postfix e 2 0
       (decisions #:var (list (λ _ 'x) (λ _ 'y))
                  #:nt (patterns third second first first))))
@@ -198,7 +215,7 @@
   (define-language var
     (e (variable-except x y)))
   (test
-   (generate/decisions
+   (generate-term
     var e 2 0
     (decisions #:var (list (λ _ 'x) (λ _ 'y) (λ _ 'x) (λ _ 'z))))
    'z))
@@ -215,25 +232,25 @@
     (n number)
     (z 4))
   (test
-   (generate/decisions 
+   (generate-term 
     lang a 2 0
     (decisions #:num (build-list 3 (λ (n) (λ (_) n)))
                #:seq (list (λ (_) 2) (λ (_) 3) (λ (_) 1))))
    `(0 1 2 "foo" "foo" "foo" "bar" #t))
-  (test (generate/decisions lang b 5 0 (decisions #:seq (list (λ (_) 0))))
+  (test (generate-term lang b 5 0 (decisions #:seq (list (λ (_) 0))))
         null)
-  (test (generate/decisions lang c 5 0 (decisions #:seq (list (λ (_) 0))))
+  (test (generate-term lang c 5 0 (decisions #:seq (list (λ (_) 0))))
         null)
-  (test (generate/decisions lang d 5 0 (decisions #:seq (list (λ (_) 2))))
+  (test (generate-term lang d 5 0 (decisions #:seq (list (λ (_) 2))))
         '(4 4 4 4 (4 4) (4 4)))
-  (test (exn:fail-message (generate lang e 5)) 
+  (test (exn:fail-message (generate-term lang e 5)) 
         #rx"generate: unable to generate pattern e")
-  (test (generate/decisions lang f 5 0 (decisions #:seq (list (λ (_) 0)))) null)
-  (test (generate/decisions lang ((0 ..._!_1) ... (1 ..._!_1) ...) 5 0
+  (test (generate-term lang f 5 0 (decisions #:seq (list (λ (_) 0)))) null)
+  (test (generate-term lang ((0 ..._!_1) ... (1 ..._!_1) ...) 5 0
                   (decisions #:seq (list (λ (_) 2) (λ (_) 3) (λ (_) 4) (λ (_) 2) (λ (_) 3) (λ (_) 4)
                                          (λ (_) 2) (λ (_) 3) (λ (_) 4) (λ (_) 1) (λ (_) 3))))
         '((0 0 0) (0 0 0 0) (1 1 1)))
-  (test (generate/decisions lang ((0 ..._!_1) ... (1 ..._!_1) ...) 5 0
+  (test (generate-term lang ((0 ..._!_1) ... (1 ..._!_1) ...) 5 0
                   (decisions #:seq (list (λ (_) 2) (λ (_) 3) (λ (_) 4) (λ (_) 2) (λ (_) 3) (λ (_) 5))))
         '((0 0 0) (0 0 0 0) (1 1 1) (1 1 1 1 1))))
 
@@ -247,7 +264,7 @@
   ;; x and y bound in body
   (test 
    (let/ec k 
-     (generate/decisions 
+     (generate-term 
       lc e 10 0
       (decisions #:var (list (λ _ 'x) (λ _ 'y) (λ (c l b a) (k b)))
                  #:nt (patterns first first first third first)
@@ -257,7 +274,7 @@
 (let ()
   (define-language lang (e (variable-prefix pf)))
   (test 
-   (generate/decisions
+   (generate-term
     lang e 5 0
     (decisions #:var (list (λ _ 'x))))
    'pfx))
@@ -271,7 +288,7 @@
   (define-language lang
     (e number (e_1 e_2 e e_1 e_2)))
   (test
-   (generate/decisions
+   (generate-term
     lang e 5 0
     (decisions #:nt (patterns second first first first)
                #:num (list (λ _ 2) (λ _ 3) (λ _ 4))))
@@ -283,7 +300,7 @@
     (x variable))
   (test
    (let/ec k
-     (generate/decisions
+     (generate-term
       lang e 5 0
       (decisions #:var (list (λ _ 'x) (λ (c l b a) (k b))))))
    '(x)))
@@ -294,17 +311,17 @@
     (b (c_!_1 c_!_1 c_!_1))
     (c 1 2))
   (test
-   (generate/decisions
+   (generate-term
     lang a 5 0
     (decisions #:num (list (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 2))))
    '(1 1 2))
   (test
-   (generate/decisions
+   (generate-term
     lang (number_!_1 number_!_2 number_!_1) 5 0
     (decisions #:num (list (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 1) (λ _ 2))))
    '(1 1 2))
   (test
-   (exn:fail-message (generate lang b 5000))
+   (exn:fail-message (generate-term lang b 5000))
    #rx"unable"))
 
 (let ()
@@ -313,7 +330,7 @@
     (f foo bar))
   (test
    (let/ec k 
-     (generate/decisions 
+     (generate-term 
       lang e 5 0 
       (decisions #:str (list (λ (c l a) (k (cons (sort c char<=?) (sort l string<=?))))))))
    (cons '(#\a #\b #\f #\o #\r)
@@ -327,28 +344,28 @@
     (d (side-condition (x_1 x_1 x) (not (eq? (term x_1) 'x))) #:binds x_1 x)
     (e (side-condition (x_1 x_!_2 x_!_2) (not (eq? (term x_1) 'x))))
     (x variable))
-  (test (generate lang b 5) 43)
-  (test (generate lang (side-condition a (odd? (term a))) 5) 43)
-  (test (exn:fail-message (generate lang c 5))
+  (test (generate-term lang b 5) 43)
+  (test (generate-term lang (side-condition a (odd? (term a))) 5) 43)
+  (test (exn:fail-message (generate-term lang c 5))
         #rx"unable to generate")
   (test ; binding works for with side-conditions failure/retry
    (let/ec k
-     (generate/decisions
+     (generate-term
       lang d 5 0
       (decisions #:var (list (λ _ 'x) (λ _ 'x) (λ _ 'y) (λ (c l b a) (k b))))))
    '(y))
   (test ; mismatch patterns work with side-condition failure/retry
-   (generate/decisions
+   (generate-term
     lang e 5 0
     (decisions #:var (list (λ _ 'x) (λ _ 'x) (λ _ 'y) (λ _ 'y) (λ _ 'x) (λ _ 'y))))
    '(y x y))
   (test ; generate compiles side-conditions in pattern
-   (generate/decisions lang (side-condition x_1 (not (eq? (term x_1) 'x))) 5 0
+   (generate-term lang (side-condition x_1 (not (eq? (term x_1) 'x))) 5 0
              (decisions #:var (list (λ _ 'x) (λ _ 'y))))
    'y)
   (test ; bindings within ellipses collected properly
    (let/ec k
-     (generate/decisions lang (side-condition (((number_1 3) ...) ...) (k (term ((number_1 ...) ...)))) 5 0
+     (generate-term lang (side-condition (((number_1 3) ...) ...) (k (term ((number_1 ...) ...)))) 5 0
                (decisions #:seq (list (λ (_) 2) (λ (_) 3) (λ (_) 4))
                           #:num (build-list 7 (λ (n) (λ (_) n))))))
    '((0 1 2) (3 4 5 6))))
@@ -360,9 +377,9 @@
     (c (side-condition (name x d) (zero? (term x))))
     (d 2 1 0)
     (e ((side-condition (name d_1 d) (zero? (term d_1))) d_1)))
-  (test (generate lang a 5) 4)
-  (test (generate lang c 5) 0)
-  (test (generate lang e 5) '(0 0)))
+  (test (generate-term lang a 5) 4)
+  (test (generate-term lang c 5) 0)
+  (test (generate-term lang e 5) '(0 0)))
 
 (let ()
   (define-language lang
@@ -380,28 +397,28 @@
     (y variable))
   
   (test 
-   (generate/decisions 
+   (generate-term 
     lang (in-hole A number ) 5 0
     (decisions 
      #:nt (patterns second second first first third first second first first)
      #:num (build-list 5 (λ (x) (λ (_) x)))))
    '(+ (+ 1 2) (+ 0 (+ 3 4))))
   
-  (test (generate lang (in-hole (in-hole (1 hole) hole) 5) 5) '(1 5))
-  (test (generate lang (hole 4) 5) (term (hole 4)))
-  (test (generate/decisions lang (variable_1 (in-hole C variable_1)) 5 0
+  (test (generate-term lang (in-hole (in-hole (1 hole) hole) 5) 5) '(1 5))
+  (test (generate-term lang (hole 4) 5) (term (hole 4)))
+  (test (generate-term lang (variable_1 (in-hole C variable_1)) 5 0
                   (decisions #:var (list (λ _ 'x) (λ _ 'y) (λ _ 'x))))
         '(x x))
-  (test (generate/decisions lang (variable_!_1 (in-hole C variable_!_1)) 5 0
+  (test (generate-term lang (variable_!_1 (in-hole C variable_!_1)) 5 0
                   (decisions #:var (list (λ _ 'x) (λ _ 'x) (λ _ 'x) (λ _ 'y))))
         '(x y))
-  (test (let/ec k (generate/decisions lang d 5 0 (decisions #:var (list (λ _ 'x) (λ (c l b a) (k b))))))
+  (test (let/ec k (generate-term lang d 5 0 (decisions #:var (list (λ _ 'x) (λ (c l b a) (k b))))))
         '(x))
-  (test (generate/decisions lang e 5 0 (decisions #:num (list (λ _ 1) (λ _ 2))))
+  (test (generate-term lang e 5 0 (decisions #:num (list (λ _ 1) (λ _ 2))))
         '((2 (1 1)) 1))
-  (test (generate/decisions lang g 5 0 (decisions #:num (list (λ _ 1) (λ _ 2) (λ _ 1) (λ _ 0))))
+  (test (generate-term lang g 5 0 (decisions #:num (list (λ _ 1) (λ _ 2) (λ _ 1) (λ _ 0))))
         '(1 0))
-  (test (generate/decisions lang h 5 0 (decisions #:num (list (λ _ 1) (λ _ 2) (λ _ 3))))
+  (test (generate-term lang h 5 0 (decisions #:num (list (λ _ 1) (λ _ 2) (λ _ 3))))
         '((2 ((3 (2 1)) 3)) 1)))
 
 (let ()
@@ -409,7 +426,7 @@
       (e (e e) (+ e e) x v)
       (v (λ (x) e) number)
       (x variable-not-otherwise-mentioned))
-  (test (generate/decisions lc x 5 0 (decisions #:var (list (λ _ 'λ) (λ _ '+) (λ _ 'x))))
+  (test (generate-term lc x 5 0 (decisions #:var (list (λ _ 'λ) (λ _ '+) (λ _ 'x))))
         'x))
 
 (let ()
@@ -423,14 +440,14 @@
         (list four 'f))
   (test (call-with-values (λ () (pick-any four (make-random 1))) list)
         (list sexp 'sexp))
-  (test (generate/decisions four any 5 0 (decisions #:any (list (λ _ (values four 'e))))) 4)
-  (test (generate/decisions four any 5 0 
+  (test (generate-term four any 5 0 (decisions #:any (list (λ _ (values four 'e))))) 4)
+  (test (generate-term four any 5 0 
                   (decisions #:any (list (λ _ (values sexp 'sexp)))
                              #:nt (patterns fifth second second second)
                              #:seq (list (λ _ 3))
                              #:str (list (λ _ "foo") (λ _ "bar") (λ _ "baz"))))
         '("foo" "bar" "baz"))
-  (test (generate/decisions empty any 5 0 (decisions #:nt (patterns first)
+  (test (generate-term empty any 5 0 (decisions #:nt (patterns first)
                                                      #:var (list (λ _ 'x))))
         'x))
 
@@ -438,7 +455,7 @@
 (let ()
   (define-language lang
     (e (hide-hole (in-hole ((hide-hole hole) hole) 1))))
-  (test (generate lang e 5) (term (hole 1))))
+  (test (generate-term lang e 5) (term (hole 1))))
 
 (define (output-error-port thunk)
   (let ([port (open-output-string)])
@@ -452,14 +469,11 @@
     (e x (e e) v)
     (v (λ (x) e))
     (x variable-not-otherwise-mentioned))
-  (test (generate/decisions lang (cross e) 3 0 
+  (test (generate-term lang (cross e) 3 0 
                   (decisions #:nt (patterns fourth first first second first first first)
                              #:var (list (λ _ 'x) (λ _ 'y))))
         (term (λ (x) (hole y)))))
 
-; preferred productions
-
-
 ;; current-error-port-output : (-> (-> any) string)
 (define (current-error-port-output thunk)
   (let ([p (open-output-string)])
@@ -521,6 +535,52 @@
   ;; OK -- generated from pattern (any ...)
   (test (check-metafunction-contract i) #t))
 
+;; check-reduction-relation
+(let ()
+  (define-language L
+    (e (+ e ...) number)
+    (E (+ number ... E* e ...))
+    (E* hole E*))
+  (define R
+    (reduction-relation
+     L
+     (==> (+ number ...) whatever)
+     (--> (side-condition number (even? (term number))) whatever)
+     with
+     [(--> (in-hole E a) whatever)
+      (==> a b)]))
+  (let ([generated null])
+    (test (begin
+            (check-reduction-relation 
+             R (λ (term) (set! generated (cons term generated)))
+             #:decisions (decisions #:seq (list (λ _ 0) (λ _ 0) (λ _ 0))
+                                    #:num (list (λ _ 1) (λ _ 1) (λ _ 0)))
+             #:attempts 1)
+            generated)
+          (reverse '((+ (+)) 0))))
+  (let ([S (reduction-relation L (--> 1 2 name) (--> 3 4))])
+    (test (check-reduction-relation S (λ (x) #t) #:attempts 1) #t)
+    (test (current-error-port-output 
+           (λ () (check-reduction-relation S (λ (x) #f))))
+          "checking name failed after 1 attempts:\n1\n")
+    (test (current-error-port-output 
+           (λ () (check-reduction-relation S (curry eq? 1))))
+          "checking unnamed failed after 1 attempts:\n3\n")))
+
+; check-metafunction
+(let ()
+  (define-language empty)
+  (define-metafunction empty
+    [(m 1) whatever]
+    [(m 2) whatever])
+  (let ([generated null])
+    (test (begin
+            (check-metafunction m (λ (t) (set! generated (cons t generated))) 1)
+            generated) 
+          (reverse '((1) (2)))))
+  (test (current-error-port-output (λ () (check-metafunction m (curry eq? 1))))
+        #rx"checking clause #1 failed after 1 attempt"))
+
 ;; parse/unparse-pattern
 (let-syntax ([test-match (syntax-rules () [(_ p x) (test (match x [p #t] [_ #f]) #t)])])
       (define-language lang (x variable))
diff --git a/collects/redex/private/rg.ss b/collects/redex/private/rg.ss
index 4131ea1eef..834700ce45 100644
--- a/collects/redex/private/rg.ss
+++ b/collects/redex/private/rg.ss
@@ -20,6 +20,7 @@ To do a better job of not generating programs with free variables,
          "underscore-allowed.ss"
          "term.ss"
          "error.ss"
+         "struct.ss"
          (for-syntax "rewrite-side-conditions.ss")
          (for-syntax "term-fn.ss")
          (for-syntax "reduction-semantics.ss")
@@ -83,13 +84,16 @@ To do a better job of not generating programs with free variables,
 (define (pick-string lang-chars lang-lits attempt [random random])
   (random-string lang-chars lang-lits (random-natural 1/5 random) attempt random))
 
-(define ((pick-nt pref-prods) nt prods bound-vars attempt)
-  (let* ([binders (filter (λ (x) (not (null? (rhs-var-info x)))) prods)]
+(define ((pick-nt pref-prods [random random]) name lang bound-vars attempt)
+  (let* ([prods (nt-rhs (nt-by-name lang name))]
+         [binders (filter (λ (x) (not (null? (rhs-var-info x)))) prods)]
          [do-intro-binder? (and (null? bound-vars)
                                 (not (null? binders))
                                 (try-to-introduce-binder?))])
     (cond [do-intro-binder? binders]
-          [(preferred-production? attempt) (list (hash-ref pref-prods nt))]
+          [(and (not (eq? lang sexp))
+                (preferred-production? attempt random))
+           (hash-ref pref-prods name)]
           [else prods])))
 
 (define (pick-from-list l [random random]) (list-ref l (random (length l))))
@@ -155,7 +159,7 @@ To do a better job of not generating programs with free variables,
          [zip (λ (l m) (map cons l m))])
     (map cdr (filter (λ (x) (equal? min-size (car x))) (zip sizes (nt-rhs nt))))))
 
-(define (generate* lang pat decisions@)
+(define (generate lang decisions@)
   (define-values/invoke-unit decisions@
     (import) (export decisions^))
   
@@ -164,19 +168,16 @@ To do a better job of not generating programs with free variables,
   (define base-table (find-base-cases lang))
   
   (define (generate-nt name fvt-id bound-vars size attempt in-hole state)
-    (let*-values 
-        ([(nt) (findf (λ (nt) (eq? name (nt-name nt))) 
-                      (append (compiled-lang-lang lang)
-                              (compiled-lang-cclang lang)))]
-         [(bound-vars) (append (extract-bound-vars fvt-id state) bound-vars)]
+    (let*-values
+        ([(bound-vars) (append (extract-bound-vars fvt-id state) bound-vars)]
          [(term _)
           (generate/pred 
            name
            (λ () 
              (let ([rhs (pick-from-list
                          (if (zero? size)
-                             (min-prods nt base-table)
-                             ((next-non-terminal-decision) name (nt-rhs nt) bound-vars attempt)))])
+                             (min-prods (nt-by-name lang name) base-table)
+                             ((next-non-terminal-decision) name lang bound-vars attempt)))])
                (((generate-pat bound-vars (max 0 (sub1 size)) attempt) (rhs-pattern rhs) in-hole)
                 (make-state (map fvt-entry (rhs-var-info rhs)) #hash()))))
            (λ (_ env) (mismatches-satisfied? env)))])
@@ -289,7 +290,7 @@ To do a better job of not generating programs with free variables,
       [`(hide-hole ,pattern) ((recur pattern the-hole) state)]
       [`any
        (let*-values ([(lang nt) ((next-any-decision) lang)]
-                     [(term _) ((generate* lang nt decisions@) size attempt)])
+                     [(term _) (((generate lang decisions@) nt) size attempt)])
          (values term state))]
       [(? (is-nt? lang))
        (generate-nt pat pat bound-vars size attempt in-hole state)]
@@ -355,15 +356,17 @@ To do a better job of not generating programs with free variables,
       (state-fvt state))
      (state-env state)))
   
-  (λ (size attempt)
-    (let-values ([(term state)
-                  (generate/pred 
-                   (unparse-pattern pat)
-                   (λ () 
-                     (((generate-pat null size attempt) pat the-hole)
-                      (make-state null #hash())))
-                   (λ (_ env) (mismatches-satisfied? env)))])
-      (values term (bindings (state-env state))))))
+  (λ (pat)
+    (let ([unparsed (unparse-pattern pat)])
+      (λ (size attempt)
+        (let-values ([(term state)
+                      (generate/pred 
+                       unparsed
+                       (λ () 
+                         (((generate-pat null size attempt) pat the-hole)
+                          (make-state null #hash())))
+                       (λ (_ env) (mismatches-satisfied? env)))])
+          (values term (bindings (state-env state))))))))
 
 ;; find-base-cases : compiled-language -> hash-table
 (define (find-base-cases lang)
@@ -446,6 +449,12 @@ To do a better job of not generating programs with free variables,
 (define (built-in? x)
   (and (memq x underscore-allowed) #t))
 
+;; nt-by-name : lang symbol -> nt
+(define (nt-by-name lang name)
+  (findf (λ (nt) (eq? name (nt-name nt))) 
+         (append (compiled-lang-lang lang)
+                 (compiled-lang-cclang lang))))
+
 (define named-nt-rx #rx"^([^_]+)_[^_]*$")
 (define mismatch-nt-rx #rx"([^_]+)_!_[^_]*$")
 (define named-ellipsis-rx #rx"^\\.\\.\\._[^_]*$")
@@ -591,7 +600,7 @@ To do a better job of not generating programs with free variables,
         [(struct ellipsis (name sub-pat class vars))
          (make-ellipsis name (recur sub-pat) (rewrite class)
                         (map (λ (v) (if (class? v) (rewrite v) v)) vars))]
-        [(? list?) (map (λ (p) (recur p)) pat)]
+        [(? list?) (map recur pat)]
         [_ pat]))))
 
 ;; used in generating the `any' pattern
@@ -610,15 +619,16 @@ To do a better job of not generating programs with free variables,
        (with-syntax ([(name ...) names]
                      [(name/ellipses ...) names/ellipses])
          (syntax/loc stx
-           (check-property 
-            (term-generator lang pat random-decisions)
-            (λ (_ bindings)
-              (with-handlers ([exn:fail? (λ (_) #f)])
-                (term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
-                          property)))
-            attempts))))]))
+           (or (check-property 
+                (term-generator lang pat random-decisions)
+                (λ (_ bindings)
+                  (with-handlers ([exn:fail? (λ (_) #f)])
+                    (term-let ([name/ellipses (lookup-binding bindings 'name)] ...)
+                              property)))
+                attempts)
+               (void)))))]))
 
-(define (check-property generate property attempts)
+(define (check-property generate property attempts [source #f])
   (let loop ([remaining attempts])
     (if (zero? remaining)
         #t
@@ -628,23 +638,21 @@ To do a better job of not generating programs with free variables,
             (if (property term bindings)
                 (loop (sub1 remaining))
                 (begin
-                  (fprintf (current-error-port) 
-                           "failed after ~s attempts:\n" 
-                           attempt)
-                  (pretty-print term (current-error-port)))))))))
+                  (when source
+                    (fprintf (current-error-port) "checking ~a " source))
+                  (fprintf (current-error-port) "failed after ~s attempts:\n" attempt)
+                  (pretty-print term (current-error-port))
+                  #f)))))))
 
-(define-syntax generate
+(define-syntax generate-term
   (syntax-rules ()
-    [(_ lang pat size attempt)
-     (let-values ([(term _) ((term-generator lang pat random-decisions) size attempt)])
+    [(_ lang pat size attempt decisions)
+     (let-values ([(term _) ((term-generator lang pat decisions) size attempt)])
        term)]
-    [(_ lang pat size) (generate lang pat size 0)]))
-
-(define-syntax generate/decisions
-  (syntax-rules ()
-    [(_ lang pat size attempt decisions@)
-     (let-values ([(term _) ((term-generator lang pat decisions@) size attempt)])
-       term)]))
+    [(_ lang pat size attempt)
+     (generate-term lang pat size attempt random-decisions)]
+    [(_ lang pat size)
+     (generate-term lang pat size 1)]))
 
 (define-syntax (term-generator stx)
   (syntax-case stx ()
@@ -655,10 +663,14 @@ To do a better job of not generating programs with free variables,
                      'generate #t #'pat)])
        (syntax/loc stx 
          (let ([lang (parse-language lang)])
-           (generate* 
-            lang
-            (reassign-classes (parse-pattern `pattern lang 'top-level))
-            (decisions lang)))))]))
+           ((generate lang (decisions lang))
+            (reassign-classes (parse-pattern `pattern lang 'top-level))))))]))
+
+(define-for-syntax (metafunc name stx)
+  (let ([tf (syntax-local-value name (λ () #f))])
+    (if (term-fn? tf)
+        (term-fn-get-id tf)
+        (raise-syntax-error #f "not a metafunction" stx name))))
 
 (define-syntax (check-metafunction-contract stx)
   (syntax-case stx ()
@@ -666,22 +678,64 @@ To do a better job of not generating programs with free variables,
      (syntax/loc stx (check-metafunction-contract name random-decisions))]
     [(_ name decisions)
      (identifier? #'name)
-     (with-syntax ([m (let ([tf (syntax-local-value #'name (λ () #f))])
-                        (if (term-fn? tf)
-                            (term-fn-get-id tf)
-                            (raise-syntax-error #f "not a metafunction" stx #'name)))])
+     (with-syntax ([m (metafunc #'name stx)])
        (syntax/loc stx 
         (let ([lang (parse-language (metafunc-proc-lang m))]
               [dom (metafunc-proc-dom-pat m)])
           (check-property 
-           (generate* lang
-                      (reassign-classes (parse-pattern (if dom dom '(any (... ...))) lang 'top-level))
-                      (decisions lang))
+           ((generate lang (decisions lang))
+            (reassign-classes (parse-pattern (if dom dom '(any (... ...))) lang 'top-level)))
            (λ (t _) 
              (with-handlers ([exn:fail:redex? (λ (_) #f)])
                (begin (term (name ,@t)) #t)))
            default-check-attempts))))]))
 
+(define (check-property-many lang patterns ids prop decisions attempts)
+  (let* ([lang-gen (generate lang (decisions lang))]
+         [pat-gens (map (λ (pat) (lang-gen (reassign-classes (parse-pattern pat lang 'top-level))))
+                        patterns)])
+    (for/and ([pat patterns]
+              [id ids])
+      (check-property
+       (let ([gen (lang-gen (reassign-classes (parse-pattern pat lang 'top-level)))])
+         (λ (size attempt) (gen size attempt)))
+       (λ (term _) (prop term))
+       attempts
+       id))))
+
+(define-syntax (check-metafunction stx)
+  (syntax-case stx ()
+    [(_ name property)
+     (syntax/loc stx (check-metafunction name property default-check-attempts))]
+    [(_ name property attempts)
+     (syntax/loc stx (check-metafunction name property random-decisions attempts))]
+    [(_ name property decisions attempts)
+     (with-syntax ([m (metafunc #'name stx)])
+       (syntax/loc stx
+         (or (check-property-many
+              (parse-language (metafunc-proc-lang m))
+              (metafunc-proc-lhs-pats m)
+              (build-list (length (metafunc-proc-lhs-pats m))
+                          (compose (curry format "clause #~s") add1))
+              property
+              decisions
+              attempts)
+             (void))))]))
+
+(define (check-reduction-relation 
+         relation property 
+         #:decisions [decisions random-decisions]
+         #:attempts [attempts default-check-attempts])
+  (or (check-property-many
+       (parse-language (reduction-relation-lang relation))
+       (map rewrite-proc-lhs (reduction-relation-make-procs relation))
+       (map (λ (proc) (or (rewrite-proc-name proc) 'unnamed))
+            (reduction-relation-make-procs relation))
+       property
+       decisions
+       attempts)
+      (void)))
+
 (define-signature decisions^
   (next-variable-decision
    next-number-decision
@@ -693,7 +747,7 @@ To do a better job of not generating programs with free variables,
 (define (random-decisions lang)
   (define preferred-productions
     (make-immutable-hasheq
-     (map (λ (nt) (cons (nt-name nt) (pick-from-list (nt-rhs nt))))
+     (map (λ (nt) (cons (nt-name nt) (list (pick-from-list (nt-rhs nt)))))
           (append (compiled-lang-lang lang)
                   (compiled-lang-cclang lang)))))
   (unit (import) (export decisions^)
@@ -705,12 +759,13 @@ To do a better job of not generating programs with free variables,
         (define (next-string-decision) pick-string)))
 
 (provide pick-from-list pick-var min-prods decisions^ pick-sequence-length
-         is-nt? pick-char random-string pick-string check
-         pick-nt unique-chars pick-any sexp generate parse-pattern
+         is-nt? pick-char random-string pick-string check nt-by-name
+         pick-nt unique-chars pick-any sexp generate-term parse-pattern
          class-reassignments reassign-classes unparse-pattern
          (struct-out ellipsis) (struct-out mismatch) (struct-out class)
-         (struct-out binder) generate/decisions check-metafunction-contract
-         pick-number parse-language)
+         (struct-out binder) check-metafunction-contract
+         pick-number parse-language check-reduction-relation 
+         preferred-production-threshold check-metafunction)
 
 (provide/contract
  [find-base-cases (-> compiled-lang? hash?)])
\ No newline at end of file
diff --git a/collects/redex/private/struct.ss b/collects/redex/private/struct.ss
index 794a3d1efe..27cba96f84 100644
--- a/collects/redex/private/struct.ss
+++ b/collects/redex/private/struct.ss
@@ -9,7 +9,7 @@
          build-reduction-relation
          reduction-relation?
          empty-reduction-relation
-         make-rewrite-proc rewrite-proc? rewrite-proc-name
+         make-rewrite-proc rewrite-proc? rewrite-proc-name rewrite-proc-lhs
          (struct-out rule-pict))
 
 (define-struct rule-pict (arrow lhs rhs label side-conditions fresh-vars pattern-binds))
@@ -20,13 +20,14 @@
 ;;   we want to avoid doing it multiple times, so it is cached in a reduction-relation struct
 
 
-(define-values (make-rewrite-proc rewrite-proc? rewrite-proc-name)
+(define-values (make-rewrite-proc rewrite-proc? rewrite-proc-name rewrite-proc-lhs)
   (let ()
     (define-values (type constructor predicate accessor mutator) 
-      (make-struct-type 'rewrite-proc #f 2 0 #f '() #f 0))
+      (make-struct-type 'rewrite-proc #f 3 0 #f '() #f 0))
     (values constructor 
             predicate 
-            (make-struct-field-accessor accessor 1 'name))))
+            (make-struct-field-accessor accessor 1 'name)
+            (make-struct-field-accessor accessor 2 'lhs))))
 
 ;; lang : compiled-language
 ;; make-procs = (listof (compiled-lang -> proc))
diff --git a/collects/redex/private/tl-test.ss b/collects/redex/private/tl-test.ss
index a41fd809d0..db8b0ea187 100644
--- a/collects/redex/private/tl-test.ss
+++ b/collects/redex/private/tl-test.ss
@@ -1,6 +1,9 @@
 (module tl-test mzscheme
   (require "../reduction-semantics.ss"
-           "test-util.ss")
+           "test-util.ss"
+           (only "matcher.ss" make-bindings make-bind)
+           scheme/match
+           "struct.ss")
   
   (reset-count)
   
@@ -537,6 +540,19 @@
         (list '((2 3) 20)
               '(6 (4 5))))
   
+  ; shortcuts like this fail if compilation fails to preserve
+  ; lexical context for side-conditions expressions.
+  (test (let ([x #t])
+          (apply-reduction-relation
+           (reduction-relation
+            grammar
+            (==> variable variable)
+            with
+            [(--> (a (side-condition number x)) b)
+             (==> a b)])
+           '(x 4)))
+        '(x))
+  
   (test (apply-reduction-relation/tag-with-names
          (reduction-relation 
           grammar
@@ -1099,4 +1115,48 @@
          'x)
         '(x1))
   
+  (let ([r (reduction-relation
+            grammar
+            (->1 1 2)
+            (->2 3 4)
+            (->4 5 6)
+            with
+            [(--> (side-condition (a number) (even? (term number))) b)
+             (->1 a b)]
+            [(--> (X 
+                   (number number)
+                   (X_1 X_1)
+                   (M_!_1 M_!_1)
+                   (1 ..._1 1 ..._1)
+                   (1 ..._!_1 1 ..._!_1))
+                  b)
+             (->2 X b)]
+            [(--> (a 1) b)
+             (->3 a b)]
+            [(->3 (a 2) b)
+             (->4 a b)])])
+    
+    ; test that names are properly bound for side-conditions in shortcuts
+    (let* ([lhs (rewrite-proc-lhs (first (reduction-relation-make-procs r)))]
+           [proc (third lhs)]
+           [name (cadadr lhs)]
+           [bind (λ (n) (make-bindings (list (make-bind name n))))])
+      (test (and (proc (bind 4)) (not (proc (bind 3)))) #t))
+    
+    ; test binder renaming
+    (let ([sym-mtch? (λ (rx) (λ (s) (and (symbol? s) (regexp-match? rx (symbol->string s)))))])
+      (match (rewrite-proc-lhs (second (reduction-relation-make-procs r)))
+        [`(3
+           (,(and n1 (? (sym-mtch? #px"^number_\\d+$"))) ,n1)
+           (,(and n2 (? (sym-mtch? #px"^X_1\\d+$"))) ,n2)
+           (,(and m1 (? (sym-mtch? #px"^M_!_1\\d+$"))) ,m1)
+           (1 ,(and ...1 (? (sym-mtch? #px"^\\.\\.\\._1\\d+$"))) 1 ,...1)
+           (1 ,(and ...!1 (? (sym-mtch? #px"^\\.\\.\\._!_1\\d+$"))) 1 ,...!1))
+         #t]
+        [else #f]))
+    
+    ; test shortcut in terms of shortcut
+    (test (rewrite-proc-lhs (third (reduction-relation-make-procs r)))
+          '((5 2) 1)))
+  
   (print-tests-passed 'tl-test.ss))