diff --git a/collects/redex/pict.rkt b/collects/redex/pict.rkt
index 2068d1d33b..2b41086693 100644
--- a/collects/redex/pict.rkt
+++ b/collects/redex/pict.rkt
@@ -82,7 +82,7 @@
   (parameter/c reduction-rule-style/c)]
  [arrow-space (parameter/c natural-number/c)]
  [label-space (parameter/c natural-number/c)]
- [metafunction-cases (parameter/c (or/c #f (and/c pair? (listof (and/c integer? (or/c zero? positive?))))))]
+ [metafunction-cases (parameter/c (or/c #f (and/c pair? (listof (or/c exact-nonnegative-integer? string?)))))]
  [judgment-form-cases (parameter/c (or/c #f (and/c (listof (or/c exact-nonnegative-integer? string?))
                                                    pair?)))]
  [metafunction-pict-style 
diff --git a/collects/redex/private/pict.rkt b/collects/redex/private/pict.rkt
index 3fd290c0ea..f3c50a7830 100644
--- a/collects/redex/private/pict.rkt
+++ b/collects/redex/private/pict.rkt
@@ -4,6 +4,7 @@
          racket/class
          racket/match
          racket/pretty
+         racket/set
          (only-in racket/list drop-right last partition)
          
          texpict/mrpict
@@ -786,29 +787,38 @@
 
 (define metafunction-pict-style (make-parameter 'left-right))
 (define metafunction-cases (make-parameter #f))
-(define (select-mf-cases eqns)
-  (let ([cases (metafunction-cases)])
-    (if cases
-        (let loop ([eqns eqns]
-                   [cases (remove-dups (sort cases <))]
-                   [i 0])
-          (cond
-            [(null? eqns) null]
-            [(null? cases) null]
-            [else 
+(define (select-mf-cases eqns case-labelss)
+  (define mf-cases (metafunction-cases))
+  (cond
+    [mf-cases
+     (define i 0)
+     (define sorted-cases (remove-dups (sort (filter number? mf-cases) <)))
+     (define named-cases (apply set (filter string? mf-cases)))
+     (apply 
+      append
+      (for/list ([eqns (in-list eqns)]
+                 [case-labels (in-list case-labelss)])
+        (filter
+         values
+         (for/list ([eqn (in-list eqns)]
+                    [case-label (in-list case-labels)])
+           (begin0
              (cond
-               [(= i (car cases))
-                (cons (car eqns)
-                      (loop (cdr eqns) (cdr cases) (+ i 1)))]
-               [else
-                (loop (cdr eqns) cases (+ i 1))])]))
-        eqns)))
+               [(and (pair? sorted-cases) (= i (car sorted-cases)))
+                (set! sorted-cases (cdr sorted-cases))
+                eqn]
+               [(set-member? named-cases case-label)
+                eqn]
+               [else #f])
+             (set! i (+ i 1)))))))]
+    [else (apply append eqns)]))
 
 (define judgment-form-cases (make-parameter #f))
 (define (select-jf-cases eqns conclusions eqn-names)
   (define cases
     (or (judgment-form-cases)
-        (metafunction-cases)))
+        (and (metafunction-cases)
+             (filter number? (metafunction-cases)))))
   (cond
     [cases
      (define-values (rev-eqns rev-concs rev-eqn-names)
@@ -845,46 +855,46 @@
                                (metafunc-proc-lang (metafunction-proc mf))))
                   mfs)
     (error name "expected metafunctions that are all drawn from the same language"))
-  (let* ([current-linebreaks (linebreaks)]
-         [all-nts (language-nts (metafunc-proc-lang (metafunction-proc (car mfs))))]
-         [sep 2]
-         [style (metafunction-pict-style)]
-         [wrapper->pict (lambda (lw) (lw->pict all-nts lw))]
-         [all-eqns (apply append (map (λ (mf) (metafunc-proc-pict-info (metafunction-proc mf))) mfs))]
-         [all-lhss 
-          (apply append
-                 (map (λ (mf)
-                        (map (lambda (eqn) 
-                               (wrapper->pict
-                                (metafunction-call (metafunc-proc-name (metafunction-proc mf))
-                                                   (list-ref eqn 0))))
-                             (metafunc-proc-pict-info (metafunction-proc mf))))
-                      mfs))]
-         [eqns (select-mf-cases all-eqns)]
-         [lhss (select-mf-cases all-lhss)]
-         [rhss (map (lambda (eqn) (wrapper->pict (list-ref eqn 2))) eqns)]
-         [_ (unless (or (not current-linebreaks)
-                        (= (length current-linebreaks) (length eqns)))
-              (error 'metafunction->pict "expected the current-linebreaks parameter to be a list whose length matches the number of cases in the metafunction (~a), but got ~s"
-                     (length eqns)
-                     current-linebreaks))]
-         [linebreak-list (or current-linebreaks
-                             (map (lambda (x) #f) eqns))]
-         [mode (case style
+  (define current-linebreaks (linebreaks))
+  (define all-nts (language-nts (metafunc-proc-lang (metafunction-proc (car mfs)))))
+  (define sep 2)
+  (define style (metafunction-pict-style))
+  (define (wrapper->pict lw) (lw->pict all-nts lw))
+  (define all-eqns (map (λ (mf) (metafunc-proc-pict-info (metafunction-proc mf))) mfs))
+  (define all-lhss 
+    (map (λ (mf)
+           (map (lambda (eqn) 
+                  (wrapper->pict
+                   (metafunction-call (metafunc-proc-name (metafunction-proc mf))
+                                      (list-ref eqn 0))))
+                (metafunc-proc-pict-info (metafunction-proc mf))))
+         mfs))
+  (define case-labels (map (λ (mf) (metafunc-proc-clause-names (metafunction-proc mf))) mfs))
+  (define eqns (select-mf-cases all-eqns case-labels))
+  (define lhss (select-mf-cases all-lhss case-labels))
+  (define rhss (map (lambda (eqn) (wrapper->pict (list-ref eqn 2))) eqns))
+  (unless (or (not current-linebreaks)
+              (= (length current-linebreaks) (length eqns)))
+    (error 'metafunction->pict "expected the current-linebreaks parameter to be a list whose length matches the number of cases in the metafunction (~a), but got ~s"
+           (length eqns)
+           current-linebreaks))
+  (define linebreak-list (or current-linebreaks
+                             (map (lambda (x) #f) eqns)))
+  (define mode (case style
                  [(left-right left-right/vertical-side-conditions left-right/compact-side-conditions left-right/beside-side-conditions)
                   'horizontal]
                  [(up-down up-down/vertical-side-conditions up-down/compact-side-conditions) 'vertical]
-                 [else (error 'metafunctions->pict "unknown mode")])]
-         [=-pict (make-=)]
-         [vertical-side-conditions?
-          (memq style '(up-down/vertical-side-conditions
-                        left-right/vertical-side-conditions
-                        left-right*/vertical-side-conditions))]
-         [compact-side-conditions? 
-          (memq style '(up-down/compact-side-conditions
-                        left-right/compact-side-conditions
-                        left-right*/compact-side-conditions))]
-         [max-line-w/pre-sc (and
+                 [else (error 'metafunctions->pict "unknown mode")]))
+  (define =-pict (make-=))
+  (define vertical-side-conditions?
+    (memq style '(up-down/vertical-side-conditions
+                  left-right/vertical-side-conditions
+                  left-right*/vertical-side-conditions)))
+  (define compact-side-conditions? 
+    (memq style '(up-down/compact-side-conditions
+                  left-right/compact-side-conditions
+                  left-right*/compact-side-conditions)))
+  (define max-line-w/pre-sc (and
                              compact-side-conditions?
                              (apply
                               max
@@ -899,112 +909,111 @@
                                       [else
                                        (+ (pict-width lhs) (pict-width rhs) (pict-width =-pict)
                                           (* 2 sep))]))
-                                   lhss rhss linebreak-list)))]
-         [scs (map (lambda (eqn)
-                     (let ([scs (reverse (list-ref eqn 1))])
-                       (if (null? scs)
-                           #f
-                           (let-values ([(fresh where/sc) (partition metafunc-extra-fresh? scs)])
-                             (side-condition-pict (foldl (λ (clause picts) 
-                                                            (foldr (λ (l ps) (cons (wrapper->pict l) ps))
-                                                                   picts (metafunc-extra-fresh-vars clause)))
-                                                         '() fresh)
-                                                  (map (match-lambda
-                                                        [(struct metafunc-extra-where (lhs rhs))
-                                                         (where-pict (wrapper->pict lhs) (wrapper->pict rhs))]
-                                                        [(struct metafunc-extra-side-cond (expr))
-                                                         (wrapper->pict expr)])
-                                                       where/sc)
-                                                  (cond
-                                                   [vertical-side-conditions? 
-                                                    ;; maximize line breaks:
-                                                    0]
-                                                   [compact-side-conditions?
-                                                    ;; maximize line break as needed:
-                                                    max-line-w/pre-sc]
-                                                   [else 
-                                                    ;; no line breaks:
-                                                    +inf.0]))))))
-                   eqns)])
-    (case mode
-      [(horizontal)
-       (define (adjust-for-fills rows)
-         ;; Some rows have the form (list <pict> 'fill 'fill),
-         ;; in which case we want the <pict> to span all columns.
-         ;; To do that, we need to know the total width of the first
-         ;; two columns of non-spanning rows.
-         (define max-w-before-rhs (apply 
-                                   max
-                                   (map (lambda (row)
-                                          (match row
-                                            [(list lhs 'fill 'fill)
-                                             (+ sep sep)]
-                                            [else
-                                             (+ (pict-width (car row))
-                                                sep
-                                                (pict-width (cadr row))
-                                                sep)]))
-                                        rows)))
-         (apply
-          append
-          (map (lambda (row)
-                 (match row
-                   [(list lhs 'fill 'fill)
-                    (list
-                     ;; pretend that content is zero-width:
-                     (inset lhs 0 0 (- (pict-width lhs)) 0)
-                     (blank)
-                     ;; blank that's wide enough to ensure that the
-                     ;; right column covers the spanning pict
-                     ;; (and no more)
-                     (blank (max 0 (- (pict-width lhs) max-w-before-rhs))
-                            0))]
-                   [else row]))
-               rows)))
-       (table 3
-              (adjust-for-fills
-               (apply append
-                      (map (lambda (lhs sc rhs linebreak?)
-                             (append
-                              (list
-                               (cond
-                                [linebreak?
-                                 (list lhs 'fill 'fill)]
-                                [(and sc (eq? style 'left-right/beside-side-conditions))
-                                 (list lhs =-pict (htl-append 10 rhs sc))]
-                                [else
-                                 (list lhs =-pict rhs)]))
-                              (if linebreak?
-                                  (list
-                                   (list (htl-append sep =-pict rhs)
-                                         'fill
-                                         'fill))
-                                  null)
-                              (if (or (not sc)
-                                      (and (not linebreak?)
-                                           (eq? style 'left-right/beside-side-conditions)))
-                                  null
-                                  (list
-                                   (list sc 'fill 'fill)))))
-                           lhss
-                           scs
-                           rhss
-                           linebreak-list)))
-               ltl-superimpose ltl-superimpose
-               sep sep)]
-      [(vertical)
-       (apply vl-append
-              sep
-              (apply append
-                     (map (lambda (lhs sc rhs)
-                            (cons
-                             (vl-append (htl-append lhs =-pict) rhs)
-                             (if (not sc)
-                                 null
-                                 (list sc))))
-                          lhss
-                          scs
-                          rhss)))])))
+                                   lhss rhss linebreak-list))))
+  (define scs (for/list ([eqn (in-list eqns)])
+                (let ([scs (reverse (list-ref eqn 1))])
+                  (if (null? scs)
+                      #f
+                      (let-values ([(fresh where/sc) (partition metafunc-extra-fresh? scs)])
+                        (side-condition-pict (foldl (λ (clause picts) 
+                                                      (foldr (λ (l ps) (cons (wrapper->pict l) ps))
+                                                             picts (metafunc-extra-fresh-vars clause)))
+                                                    '() fresh)
+                                             (map (match-lambda
+                                                    [(struct metafunc-extra-where (lhs rhs))
+                                                     (where-pict (wrapper->pict lhs) (wrapper->pict rhs))]
+                                                    [(struct metafunc-extra-side-cond (expr))
+                                                     (wrapper->pict expr)])
+                                                  where/sc)
+                                             (cond
+                                               [vertical-side-conditions? 
+                                                ;; maximize line breaks:
+                                                0]
+                                               [compact-side-conditions?
+                                                ;; maximize line break as needed:
+                                                max-line-w/pre-sc]
+                                               [else 
+                                                ;; no line breaks:
+                                                +inf.0])))))))
+  (case mode
+    [(horizontal)
+     (define (adjust-for-fills rows)
+       ;; Some rows have the form (list <pict> 'fill 'fill),
+       ;; in which case we want the <pict> to span all columns.
+       ;; To do that, we need to know the total width of the first
+       ;; two columns of non-spanning rows.
+       (define max-w-before-rhs (apply 
+                                 max
+                                 (map (lambda (row)
+                                        (match row
+                                          [(list lhs 'fill 'fill)
+                                           (+ sep sep)]
+                                          [else
+                                           (+ (pict-width (car row))
+                                              sep
+                                              (pict-width (cadr row))
+                                              sep)]))
+                                      rows)))
+       (apply
+        append
+        (map (lambda (row)
+               (match row
+                 [(list lhs 'fill 'fill)
+                  (list
+                   ;; pretend that content is zero-width:
+                   (inset lhs 0 0 (- (pict-width lhs)) 0)
+                   (blank)
+                   ;; blank that's wide enough to ensure that the
+                   ;; right column covers the spanning pict
+                   ;; (and no more)
+                   (blank (max 0 (- (pict-width lhs) max-w-before-rhs))
+                          0))]
+                 [else row]))
+             rows)))
+     (table 3
+            (adjust-for-fills
+             (apply append
+                    (map (lambda (lhs sc rhs linebreak?)
+                           (append
+                            (list
+                             (cond
+                               [linebreak?
+                                (list lhs 'fill 'fill)]
+                               [(and sc (eq? style 'left-right/beside-side-conditions))
+                                (list lhs =-pict (htl-append 10 rhs sc))]
+                               [else
+                                (list lhs =-pict rhs)]))
+                            (if linebreak?
+                                (list
+                                 (list (htl-append sep =-pict rhs)
+                                       'fill
+                                       'fill))
+                                null)
+                            (if (or (not sc)
+                                    (and (not linebreak?)
+                                         (eq? style 'left-right/beside-side-conditions)))
+                                null
+                                (list
+                                 (list sc 'fill 'fill)))))
+                         lhss
+                         scs
+                         rhss
+                         linebreak-list)))
+            ltl-superimpose ltl-superimpose
+            sep sep)]
+    [(vertical)
+     (apply vl-append
+            sep
+            (apply append
+                   (map (lambda (lhs sc rhs)
+                          (cons
+                           (vl-append (htl-append lhs =-pict) rhs)
+                           (if (not sc)
+                               null
+                               (list sc))))
+                        lhss
+                        scs
+                        rhss)))]))
 
 (define (metafunction-call name an-lw)
   (struct-copy lw an-lw
diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt
index 4a816882d2..6303ab97ee 100644
--- a/collects/redex/private/reduction-semantics.rkt
+++ b/collects/redex/private/reduction-semantics.rkt
@@ -1174,6 +1174,34 @@
                     defs))
                  (syntax defs))))))]))
 
+(define-for-syntax (extract-clause-names stuffss)
+  (for/list ([stuffs (in-list (syntax->list stuffss))])
+    (define the-clause-name #f)
+    (define stuff-without-clause-name
+      (for/fold ([stuffs '()]) ([stuff+name (in-list (syntax->list stuffs))])
+        (syntax-case* stuff+name (clause-name) (λ (x y) (eq? (syntax-e x) (syntax-e y)))
+          [(clause-name id)
+           (begin
+             (unless (or (identifier? #'id)
+                         (string? (syntax-e #'id)))
+               (raise-syntax-error 'define-metafunction 
+                                   "expected an identifier or a string"
+                                   #'id))
+             (when the-clause-name
+               (raise-syntax-error 'define-metafunction
+                                   "multiple names in a single clause"
+                                   #f
+                                   #f
+                                   (list the-clause-name #'id)))
+             (set! the-clause-name #'id)
+             stuffs)]
+          [_ (cons stuff+name stuffs)])))
+    (cons (cond
+            [(not the-clause-name) #f]
+            [(identifier? the-clause-name) (symbol->string (syntax-e the-clause-name))]
+            [else the-clause-name])
+          (reverse stuff-without-clause-name))))
+
 (define-syntax (generate-metafunction stx)
   (syntax-case stx ()
     [(_ orig-stx lang prev-metafunction name name-predicate dom-ctcs codom-contracts pats syn-error-name)
@@ -1186,152 +1214,154 @@
          (definition-nts #'lang #'orig-stx syn-error-name))
        (with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats]
                      [(lhs-for-lw ...) (lhs-lws pats)])
-         (with-syntax ([((rhs stuff ...) ...) #'((raw-rhses ...) ...)]
+         (with-syntax ([((rhs stuff+names ...) ...) #'((raw-rhses ...) ...)]
                        [(lhs ...) #'((lhs-clauses ...) ...)])
-           (parse-extras #'((stuff ...) ...))
-           (with-syntax ([((side-conditions-rewritten lhs-names lhs-namess/ellipses) ...) 
-                          (map (λ (x) (rewrite-side-conditions/check-errs
-                                       lang-nts
-                                       syn-error-name
-                                       #t
-                                       x))
-                               (syntax->list (syntax (lhs ...))))])
-             (with-syntax ([(rhs/wheres ...)
-                            (map (λ (sc/b rhs names names/ellipses)
-                                   (bind-withs
-                                    syn-error-name '()  
-                                    #'effective-lang lang-nts
-                                    sc/b 'flatten
-                                    #`(list (term #,rhs #:lang lang))
-                                    (syntax->list names) 
-                                    (syntax->list names/ellipses)
-                                    #t
-                                    #f))
-                                 (syntax->list #'((stuff ...) ...))
-                                 (syntax->list #'(rhs ...))
-                                 (syntax->list #'(lhs-names ...))
-                                 (syntax->list #'(lhs-namess/ellipses ...)))]
-                           [(rg-rhs/wheres ...)
-                            (map (λ (sc/b rhs names names/ellipses) 
-                                   (bind-withs
-                                    syn-error-name '()  
-                                    #'effective-lang lang-nts
-                                    sc/b 'predicate
-                                    #`#t
-                                    (syntax->list names)
-                                    (syntax->list names/ellipses)
-                                    #t
-                                    #f))
-                                 (syntax->list #'((stuff ...) ...))
-                                 (syntax->list #'(rhs ...))
-                                 (syntax->list #'(lhs-names ...))
-                                 (syntax->list #'(lhs-namess/ellipses ...)))])
-               (with-syntax ([((rg-side-conditions-rewritten rg-names rg-names/ellipses ...) ...)
-                              (map (λ (x) (rewrite-side-conditions/check-errs
-                                           lang-nts
-                                           syn-error-name
-                                           #t
-                                           x))
-                                   (syntax->list (syntax ((side-condition lhs rg-rhs/wheres) ...))))]
-                             [(clause-src ...)
-                              (map (λ (lhs)
-                                     (format "~a:~a:~a"
-                                             (and (path? (syntax-source lhs))
-                                                  (path->relative-string/library (syntax-source lhs)))
-                                             (syntax-line lhs)
-                                             (syntax-column lhs)))
-                                   pats)]
-                             [(dom-side-conditions-rewritten dom-names dom-names/ellipses)
-                              (if dom-ctcs
-                                  (rewrite-side-conditions/check-errs
-                                   lang-nts
-                                   syn-error-name
-                                   #f
-                                   dom-ctcs)
-                                  #'(any () ()))]
-                             [((codom-side-conditions-rewritten codom-names codom-names/ellipses) ...)
-                              (map (λ (codom-contract)
-                                     (rewrite-side-conditions/check-errs
-                                      lang-nts
-                                      syn-error-name
-                                      #f
-                                      codom-contract))
-                                   codom-contracts)]
-                             [(rhs-fns ...)
-                              (map (λ (names names/ellipses rhs/where)
-                                     (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))))))
+           (with-syntax ([((clause-name stuff ...) ...) (extract-clause-names #'((stuff+names ...) ...))])
+             (parse-extras #'((stuff ...) ...))
+             (with-syntax ([((side-conditions-rewritten lhs-names lhs-namess/ellipses) ...) 
+                            (map (λ (x) (rewrite-side-conditions/check-errs
+                                         lang-nts
+                                         syn-error-name
+                                         #t
+                                         x))
+                                 (syntax->list (syntax (lhs ...))))])
+               (with-syntax ([(rhs/wheres ...)
+                              (map (λ (sc/b rhs names names/ellipses)
+                                     (bind-withs
+                                      syn-error-name '()  
+                                      #'effective-lang lang-nts
+                                      sc/b 'flatten
+                                      #`(list (term #,rhs #:lang lang))
+                                      (syntax->list names) 
+                                      (syntax->list names/ellipses)
+                                      #t
+                                      #f))
+                                   (syntax->list #'((stuff ...) ...))
+                                   (syntax->list #'(rhs ...))
                                    (syntax->list #'(lhs-names ...))
-                                   (syntax->list #'(lhs-namess/ellipses ...))
-                                   (syntax->list (syntax (rhs/wheres ...))))]
-                             [((gen-clause lhs-pat) ...)
-                              (make-mf-clauses (syntax->list #'(lhs ...))
-                                               (syntax->list #'(rhs ...))
-                                               (syntax->list #'((stuff ...) ...))
-                                               lang-nts syn-error-name #'name #'lang)])
-                 (syntax-property
-                  (prune-syntax
-                   #`(let ([sc `(side-conditions-rewritten ...)]
-                           [dsc `dom-side-conditions-rewritten])
-                       (let ([cases (map (λ (pat rhs-fn rg-lhs src)
-                                           (make-metafunc-case
-                                            (λ (effective-lang) (compile-pattern effective-lang pat #t))
-                                            rhs-fn
-                                            rg-lhs src (gensym)))
-                                         sc
-                                         (list (λ (effective-lang) rhs-fns) ...)
-                                         (list (λ (effective-lang) `rg-side-conditions-rewritten) ...)
-                                         `(clause-src ...))]
-                             [parent-cases 
-                              #,(if prev-metafunction
-                                    #`(metafunc-proc-cases #,(term-fn-get-id (syntax-local-value prev-metafunction)))
-                                    #'null)]
-                             [new-lhs-pats '(lhs-pat ...)])
-                         (build-metafunction 
-                          lang
-                          cases
-                          parent-cases
-                          (λ (f/dom)
-                            (make-metafunc-proc
-                             (let ([name (lambda (x) (f/dom x))]) name)
-                             (generate-lws #f
-                                           (lhs ...)
-                                           (lhs-for-lw ...)
-                                           ((stuff ...) ...)
-                                           (rhs ...)
-                                           #t)
-                             lang
-                             #t ;; multi-args?
-                             'name
-                             (let ([name (lambda (x) (name-predicate x))]) name)
-                             dsc
-                             (append cases parent-cases)
-                             #,(cond
-                                 [prev-metafunction
-                                  #`(extend-mf-clauses #,(term-fn-get-id (syntax-local-value prev-metafunction))
-                                                       (λ ()
-                                                         #,(check-pats #'(list gen-clause ...)))
-                                                       new-lhs-pats)]
-                                 [else
-                                  #`(memoize0
-                                     (λ ()
-                                       #,(check-pats #'(list gen-clause ...))))])
-                             #,(if prev-metafunction
-                                   #`(extend-lhs-pats #,(term-fn-get-id (syntax-local-value prev-metafunction))
-                                                      new-lhs-pats)
-                                   #`new-lhs-pats)))
-                          #,(if dom-ctcs #'dsc #f)
-                          `(codom-side-conditions-rewritten ...)
-                          'name))))
-                  'disappeared-use
-                  (map syntax-local-introduce 
-                       (syntax->list #'(original-names ...))))))))))]))
+                                   (syntax->list #'(lhs-namess/ellipses ...)))]
+                             [(rg-rhs/wheres ...)
+                              (map (λ (sc/b rhs names names/ellipses) 
+                                     (bind-withs
+                                      syn-error-name '()  
+                                      #'effective-lang lang-nts
+                                      sc/b 'predicate
+                                      #`#t
+                                      (syntax->list names)
+                                      (syntax->list names/ellipses)
+                                      #t
+                                      #f))
+                                   (syntax->list #'((stuff ...) ...))
+                                   (syntax->list #'(rhs ...))
+                                   (syntax->list #'(lhs-names ...))
+                                   (syntax->list #'(lhs-namess/ellipses ...)))])
+                 (with-syntax ([((rg-side-conditions-rewritten rg-names rg-names/ellipses ...) ...)
+                                (map (λ (x) (rewrite-side-conditions/check-errs
+                                             lang-nts
+                                             syn-error-name
+                                             #t
+                                             x))
+                                     (syntax->list (syntax ((side-condition lhs rg-rhs/wheres) ...))))]
+                               [(clause-src ...)
+                                (map (λ (lhs)
+                                       (format "~a:~a:~a"
+                                               (and (path? (syntax-source lhs))
+                                                    (path->relative-string/library (syntax-source lhs)))
+                                               (syntax-line lhs)
+                                               (syntax-column lhs)))
+                                     pats)]
+                               [(dom-side-conditions-rewritten dom-names dom-names/ellipses)
+                                (if dom-ctcs
+                                    (rewrite-side-conditions/check-errs
+                                     lang-nts
+                                     syn-error-name
+                                     #f
+                                     dom-ctcs)
+                                    #'(any () ()))]
+                               [((codom-side-conditions-rewritten codom-names codom-names/ellipses) ...)
+                                (map (λ (codom-contract)
+                                       (rewrite-side-conditions/check-errs
+                                        lang-nts
+                                        syn-error-name
+                                        #f
+                                        codom-contract))
+                                     codom-contracts)]
+                               [(rhs-fns ...)
+                                (map (λ (names names/ellipses rhs/where)
+                                       (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 #'(lhs-names ...))
+                                     (syntax->list #'(lhs-namess/ellipses ...))
+                                     (syntax->list (syntax (rhs/wheres ...))))]
+                               [((gen-clause lhs-pat) ...)
+                                (make-mf-clauses (syntax->list #'(lhs ...))
+                                                 (syntax->list #'(rhs ...))
+                                                 (syntax->list #'((stuff ...) ...))
+                                                 lang-nts syn-error-name #'name #'lang)])
+                   (syntax-property
+                    (prune-syntax
+                     #`(let ([sc `(side-conditions-rewritten ...)]
+                             [dsc `dom-side-conditions-rewritten])
+                         (let ([cases (map (λ (pat rhs-fn rg-lhs src)
+                                             (make-metafunc-case
+                                              (λ (effective-lang) (compile-pattern effective-lang pat #t))
+                                              rhs-fn
+                                              rg-lhs src (gensym)))
+                                           sc
+                                           (list (λ (effective-lang) rhs-fns) ...)
+                                           (list (λ (effective-lang) `rg-side-conditions-rewritten) ...)
+                                           `(clause-src ...))]
+                               [parent-cases 
+                                #,(if prev-metafunction
+                                      #`(metafunc-proc-cases #,(term-fn-get-id (syntax-local-value prev-metafunction)))
+                                      #'null)]
+                               [new-lhs-pats '(lhs-pat ...)])
+                           (build-metafunction 
+                            lang
+                            cases
+                            parent-cases
+                            (λ (f/dom)
+                              (make-metafunc-proc
+                               (let ([name (lambda (x) (f/dom x))]) name)
+                               '(clause-name ...)
+                               (generate-lws #f
+                                             (lhs ...)
+                                             (lhs-for-lw ...)
+                                             ((stuff ...) ...)
+                                             (rhs ...)
+                                             #t)
+                               lang
+                               #t ;; multi-args?
+                               'name
+                               (let ([name (lambda (x) (name-predicate x))]) name)
+                               dsc
+                               (append cases parent-cases)
+                               #,(cond
+                                   [prev-metafunction
+                                    #`(extend-mf-clauses #,(term-fn-get-id (syntax-local-value prev-metafunction))
+                                                         (λ ()
+                                                           #,(check-pats #'(list gen-clause ...)))
+                                                         new-lhs-pats)]
+                                   [else
+                                    #`(memoize0
+                                       (λ ()
+                                         #,(check-pats #'(list gen-clause ...))))])
+                               #,(if prev-metafunction
+                                     #`(extend-lhs-pats #,(term-fn-get-id (syntax-local-value prev-metafunction))
+                                                        new-lhs-pats)
+                                     #`new-lhs-pats)))
+                            #,(if dom-ctcs #'dsc #f)
+                            `(codom-side-conditions-rewritten ...)
+                            'name))))
+                    'disappeared-use
+                    (map syntax-local-introduce 
+                         (syntax->list #'(original-names ...)))))))))))]))
 
 (define (extend-lhs-pats old-m new-pats)
   (append new-pats (metafunc-proc-lhs-pats old-m)))
@@ -1443,7 +1473,7 @@
                                  #'form-name))]
           [_
            (raise-syntax-error 'define-metafunction 
-                               "expected a side-condition or where clause"
+                               "expected a side-condition, where, or clause-name"
                                stuff)]))
       (syntax->list stuffs)))
    (syntax->list extras)))
@@ -2313,6 +2343,7 @@
          metafunction? metafunction-proc
          in-domain?
          metafunc-proc-lang
+         metafunc-proc-clause-names
          metafunc-proc-pict-info
          metafunc-proc-name
          metafunc-proc-multi-arg?
diff --git a/collects/redex/private/term-fn.rkt b/collects/redex/private/term-fn.rkt
index 839d76b73c..e346b53554 100644
--- a/collects/redex/private/term-fn.rkt
+++ b/collects/redex/private/term-fn.rkt
@@ -13,6 +13,7 @@
          defined-check
          not-expression-context
          
+         metafunc-proc-clause-names
          metafunc-proc-pict-info
          metafunc-proc-lang
          metafunc-proc-multi-arg?
@@ -72,13 +73,14 @@
                               variable-not-otherwise-mentioned hole symbol))
 
 (define-values (struct:metafunc-proc make-metafunc-proc metafunc-proc? metafunc-proc-ref metafunc-proc-set!)
-  (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))
-(define metafunc-proc-name (make-struct-field-accessor metafunc-proc-ref 4))
-(define metafunc-proc-in-dom? (make-struct-field-accessor metafunc-proc-ref 5))
-(define metafunc-proc-dom-pat (make-struct-field-accessor metafunc-proc-ref 6))
-(define metafunc-proc-cases (make-struct-field-accessor metafunc-proc-ref 7))
-(define metafunc-proc-gen-clauses (make-struct-field-accessor metafunc-proc-ref 8))
-(define metafunc-proc-lhs-pats (make-struct-field-accessor metafunc-proc-ref 9))
+  (make-struct-type 'metafunc-proc #f 11 0 #f null (current-inspector) 0))
+(define metafunc-proc-clause-names (make-struct-field-accessor metafunc-proc-ref 1))
+(define metafunc-proc-pict-info (make-struct-field-accessor metafunc-proc-ref 2))
+(define metafunc-proc-lang (make-struct-field-accessor metafunc-proc-ref 3))
+(define metafunc-proc-multi-arg? (make-struct-field-accessor metafunc-proc-ref 4))
+(define metafunc-proc-name (make-struct-field-accessor metafunc-proc-ref 5))
+(define metafunc-proc-in-dom? (make-struct-field-accessor metafunc-proc-ref 6))
+(define metafunc-proc-dom-pat (make-struct-field-accessor metafunc-proc-ref 7))
+(define metafunc-proc-cases (make-struct-field-accessor metafunc-proc-ref 8))
+(define metafunc-proc-gen-clauses (make-struct-field-accessor metafunc-proc-ref 9))
+(define metafunc-proc-lhs-pats (make-struct-field-accessor metafunc-proc-ref 10))
diff --git a/collects/redex/scribblings/ref.scrbl b/collects/redex/scribblings/ref.scrbl
index fb01f411b8..f7057100dd 100644
--- a/collects/redex/scribblings/ref.scrbl
+++ b/collects/redex/scribblings/ref.scrbl
@@ -1092,7 +1092,8 @@ reduce it further).
                                    (where pat @#,tttterm)
                                    (where/hidden pat @#,tttterm)
                                    (judgment-holds 
-                                    (judgment-form-id pat/term ...))])]{
+                                    (judgment-form-id pat/term ...))
+                                   (clause-name name)])]{
 
 The @racket[define-metafunction] form builds a function on
 sexpressions according to the pattern and right-hand-side
@@ -1109,6 +1110,23 @@ no clauses match, if one of the clauses matches multiple ways
 (and that leads to different results for the different matches),
 or if the contract is violated.
 
+The @racket[side-condition] extra is evaluated after a successful match
+to the corresponding argument pattern. If it returns @racket[#f],
+the clause is considered not to have matched, and the next one is tried.
+The @racket[side-condition/hidden] extra behaves the same, but is
+not typeset.
+
+The @racket[where] and @racket[where/hidden] extra are like
+@racket[side-condition] and @racket[side-condition/hidden],
+except the match guards the clause.
+
+The @racket[judgment-holds] clause is like @racket[side-condition]
+and @racket[where], except the given judgment must hold for the
+clause to be taken.
+
+The @racket[clause-name] is used only when typesetting. See
+@racket[metafunction-cases].
+
 Note that metafunctions are assumed to always return the same results
 for the same inputs, and their results are cached, unless
 @racket[caching-enabled?] is set to @racket[#f]. Accordingly, if a
@@ -2704,15 +2722,18 @@ precede ellipses that represent argument sequences; when it is
 
 @defparam[metafunction-cases 
           cases
-          (or/c #f (and/c (listof (and/c integer?
-                                         (or/c zero? positive?)))
+          (or/c #f (and/c (listof (or/c exact-nonnegative-integer? 
+                                        string?))
                           pair?))]{
 
-Controls which cases in a metafunction are rendered. If it is @racket[#f] (the default), then all of the
-cases appear. If it is a list of numbers, then only the selected cases appear (counting from @racket[0]).
+Controls which cases in a metafunction are rendered. If it is @racket[#f]
+(the default), then all of the cases appear. If it is a list, then only 
+the selected cases appear. The numbers indicate the cases counting from
+@racket[0] and the strings indicate cases named with @racket[clause-name].
 
 This parameter also controls how which clauses in judgment forms are rendered, but
-only in the case that @racket[judgment-form-cases] is @racket[#f].
+only in the case that @racket[judgment-form-cases] is @racket[#f] (and in that
+case, only the numbers are used).
 }
                                   
 @defparam[judgment-form-cases 
diff --git a/collects/redex/tests/bitmap-test.rkt b/collects/redex/tests/bitmap-test.rkt
index 3fa53cc5de..6076fd00dd 100644
--- a/collects/redex/tests/bitmap-test.rkt
+++ b/collects/redex/tests/bitmap-test.rkt
@@ -114,7 +114,8 @@
 (define-metafunction lang
   [(T x y)
    1
-   (side-condition (not (eq? (term x) (term y))))]
+   (side-condition (not (eq? (term x) (term y))))
+   (clause-name first-one)]
   [(T x x) 
    (any_1 any_2)
    (where any_1 2)
@@ -123,7 +124,9 @@
 ;; in this test, the metafunction has 2 clauses 
 ;; with a side-condition on the first clause
 ;; and a 'where' in the second clause
-(btest (render-metafunction T) "metafunction-T.png")
+(btest (parameterize ([metafunction-cases '("first-one" 1)])
+         (render-metafunction T))
+       "metafunction-T.png")
 
 ;; in this test, the `x' is italic and the 'z' is sf, since 'x' is in the grammar, and 'z' is not.
 (btest (render-lw