diff --git a/collects/redex/private/judgment-form.rkt b/collects/redex/private/judgment-form.rkt
index b863c4c033..5007448281 100644
--- a/collects/redex/private/judgment-form.rkt
+++ b/collects/redex/private/judgment-form.rkt
@@ -96,7 +96,7 @@
      (hash-set extended (syntax-e name) w/ellipses))))
 
 ;; the withs, freshs, and side-conditions come in backwards order
-(define-for-syntax (bind-withs orig-name main lang lang-nts stx where-mode body names w/ellipses side-condition-unquoted?)
+(define-for-syntax (bind-withs orig-name main lang lang-nts stx where-mode body names w/ellipses side-condition-unquoted? jf-results-id)
   (with-disappeared-uses
    (let loop ([stx stx]
               [to-not-be-in main]
@@ -211,19 +211,32 @@
                  #,lang
                  `#,output-pattern
                  #,call
-                 (λ (bindings)
+                 #,under-ellipsis?
+                 #,jf-results-id
+                 (λ (bindings #,@(if jf-results-id (list jf-results-id) '()))
                    (let ([temp (lookup-binding bindings 'output-name)] ...)
                      (and binding-constraint ...
                           (term-let ([output-name/ellipsis temp] ...) 
                                     #,rest-body))))))))]))))
 
-(define (judgment-form-bind-withs/proc lang output-pattern call-output do-something)
+(define (judgment-form-bind-withs/proc lang output-pattern output under-ellipsis? old-maps do-something)
   (let ([compiled-pattern (compile-pattern lang output-pattern #t)])
-    (for/fold ([outputs '()]) ([sub-output call-output])
-      (define mtchs (match-pattern compiled-pattern sub-output))
+    (for/fold ([outputs '()]) ([sub-output (in-list output)])
+      (define sub-tree (if under-ellipsis?
+                           (map (λ (x) (vector-ref x 0)) sub-output)
+                           (vector-ref sub-output 0)))
+      (define term (if under-ellipsis?
+                       (map (λ (x) (vector-ref x 1)) sub-output)
+                       (vector-ref sub-output 1)))
+      (define mtchs (match-pattern compiled-pattern term))
       (if mtchs
-          (for/fold ([outputs outputs]) ([mtch mtchs])
-            (define mtch-outputs (do-something (mtch-bindings mtch)))
+          (for/fold ([outputs outputs]) ([mtch (in-list mtchs)])
+            (define mtch-outputs (if old-maps
+                                     (do-something (mtch-bindings mtch) 
+                                                   (if under-ellipsis?
+                                                       (append (reverse sub-tree) old-maps)
+                                                       (cons sub-tree old-maps)))
+                                     (do-something (mtch-bindings mtch))))
             (if mtch-outputs
                 (append mtch-outputs outputs)
                 outputs))
@@ -251,18 +264,31 @@
 
 (define (call-judgment-form form-name form-proc mode input)
   (define traced (current-traced-metafunctions))
-  (if (or (eq? 'all traced) (memq form-name traced))
-      (let ([outputs #f])
-        (define spacers
-          (for/fold ([s '()]) ([m mode])
-            (case m [(I) s] [(O) (cons '_ s)])))
-        (define (wrapped . _)
-          (set! outputs (form-proc form-proc input))
-          (for/list ([output outputs])
-            (cons form-name (assemble mode input output))))
-        (apply trace-call form-name wrapped (assemble mode input spacers))
-        outputs)
-      (form-proc form-proc input)))
+  (define vecs
+    (if (or (eq? 'all traced) (memq form-name traced))
+        (let ([outputs #f])
+          (define spacers
+            (for/fold ([s '()]) ([m mode])
+              (case m [(I) s] [(O) (cons '_ s)])))
+          (define (wrapped . _)
+            (set! outputs (form-proc form-proc input))
+            (for/list ([output outputs])
+              (cons form-name (assemble mode input (vector-ref output 1)))))
+          (apply trace-call form-name wrapped (assemble mode input spacers))
+          outputs)
+        (form-proc form-proc input)))
+  (for/list ([v (in-list vecs)])
+    (vector (derivation (cons form-name (assemble mode input (vector-ref v 1)))
+                        (reverse (vector-ref v 0)))
+            (vector-ref v 1))))
+(struct derivation (term subs) 
+  #:transparent
+  #:guard (λ (term subs name)
+            (unless (and (list? subs)
+                         (andmap derivation? subs))
+              (error name "expected the second (subs) field to be a list of derivation?s, got: ~e"
+                     subs))
+            (values term subs)))
 
 (define (assemble mode inputs outputs)
   (let loop ([ms mode] [is inputs] [os outputs])
@@ -358,7 +384,8 @@
   (define definitions
     #`(begin
         (define-syntax #,judgment-form-name 
-          (judgment-form '#,judgment-form-name '#,(cdr (syntax->datum mode)) #'judgment-form-runtime-proc #'mk-judgment-form-proc #'#,lang #'judgment-form-lws
+          (judgment-form '#,judgment-form-name '#,(cdr (syntax->datum mode)) #'judgment-form-runtime-proc
+                         #'mk-judgment-form-proc #'#,lang #'judgment-form-lws
                          '#,rule-names #'judgment-runtime-gen-clauses #'mk-judgment-gen-clauses))
         (define mk-judgment-form-proc
           (compile-judgment-form-proc #,judgment-form-name #,mode #,lang #,clauses #,position-contracts #,orig #,stx #,syn-err-name))
@@ -366,7 +393,9 @@
         (define judgment-form-lws
           (compiled-judgment-form-lws #,clauses))
         (define mk-judgment-gen-clauses
-          (compile-judgment-gen-clauses #,judgment-form-name #,mode #,lang #,clauses #,position-contracts #,orig #,stx #,syn-err-name judgment-runtime-gen-clauses))
+          (compile-judgment-gen-clauses #,judgment-form-name #,mode #,lang
+                                        #,clauses #,position-contracts #,orig
+                                        #,stx #,syn-err-name judgment-runtime-gen-clauses))
         (define judgment-runtime-gen-clauses (mk-judgment-gen-clauses #,lang (λ () (judgment-runtime-gen-clauses))))))
   (syntax-property
    (values ;prune-syntax
@@ -506,27 +535,57 @@
             the-name (list (car others))))
          (loop (cdr others))]))))
 
-(define-syntax (judgment-holds stx)
+(define-syntax (judgment-holds/derivation stx)
   (syntax-case stx ()
-    [(j-h judgment)
-     #`(not (null? #,(syntax/loc stx (j-h judgment #t))))]
-    [(j-h (form-name . pats) tmpl)
+    [(_ stx-name derivation? judgment)
+     #`(not (null? #,(syntax/loc stx (judgment-holds/derivation stx-name derivation? judgment #t))))]
+    [(_ stx-name derivation? (form-name . pats) tmpl)
      (judgment-form-id? #'form-name)
-     (let* ([syn-err-name (syntax-e #'j-h)]
+     (let* ([syn-err-name (syntax-e #'stx-name)]
             [lang (judgment-form-lang (lookup-judgment-form-id #'form-name))]
             [nts (definition-nts lang stx syn-err-name)]
-            [judgment (syntax-case stx () [(_ judgment _) #'judgment])])
+            [judgment (syntax-case stx () [(_ _ _ judgment _) #'judgment])]
+            [derivation? (syntax-e #'derivation?)]
+            [id-or-not (if derivation?
+                           (car (generate-temporaries '(jf-derivation-lst)))
+                           #f)]
+            [main-stx
+             (bind-withs syn-err-name '() lang nts (list judgment)
+                         'flatten
+                         (if derivation?
+                             id-or-not
+                             #`(list (term #,#'tmpl #:lang #,lang)))
+                         '()
+                         '()
+                         #f
+                         id-or-not)])
        (check-judgment-arity stx judgment)
        (syntax-property
-        #`(sort #,(bind-withs syn-err-name '() lang nts (list judgment)
-                              'flatten #`(list (term #,#'tmpl #:lang #,lang)) '() '() #f)
-                string<=?
-                #:key (λ (x) (format "~s" x)))
+        (if id-or-not
+            #`(let ([#,id-or-not '()])
+                #,main-stx)
+            #`(sort #,main-stx
+                    string<=?
+                    #:key (λ (x) (format "~s" x))))
         'disappeared-use
         (syntax-local-introduce #'form-name)))]
-    [(_ (not-form-name . _) . _)
+    [(_ stx-name derivation? (not-form-name . _) . _)
      (not (judgment-form-id? #'form-name))
-     (raise-syntax-error #f "expected a judgment form name" stx #'not-form-name)]))
+     (raise-syntax-error (syntax-e #'stx-name) "expected a judgment form name" #'not-form-name)]
+    [(_ stx-name . whatever)
+     (raise-syntax-error (syntax-e #'stx-name)
+                         "bad syntax"
+                         stx)]))
+
+(define-syntax (judgment-holds stx)
+  (syntax-case stx ()
+    [(_  args ...)
+     #'(#%expression (judgment-holds/derivation judgment-holds #f args ...))]))
+
+(define-syntax (build-derivations stx)
+  (syntax-case stx ()
+    [(_  jf-expr)
+     #'(#%expression (judgment-holds/derivation build-derivations #t jf-expr any))]))
 
 (define-for-syntax (do-compile-judgment-form-proc name mode-stx clauses contracts nts orig stx syn-error-name)
   (define mode (cdr (syntax->datum mode-stx)))
@@ -539,7 +598,8 @@
     (syntax-case clause ()
       [((_ . conc-pats) . prems)
        (let-values ([(input-pats output-pats) (split-by-mode (syntax->list #'conc-pats) mode)])
-         (with-syntax ([(lhs (names ...) (names/ellipses ...)) (rewrite-side-conditions/check-errs nts syn-error-name #t input-pats)])
+         (with-syntax ([(lhs (names ...) (names/ellipses ...)) (rewrite-side-conditions/check-errs nts syn-error-name #t input-pats)]
+                       [(jf-derivation-id) (generate-temporaries '(jf-derivation-id))])
            (define (contracts-compilation ctcs)
              (and ctcs
                   (with-syntax ([(ctc ...) ctcs])
@@ -550,16 +610,18 @@
                                    (struct-copy judgment-form (lookup-judgment-form-id name)
                                                 [proc #'recur]))])
                (bind-withs syn-error-name '() #'lang nts (syntax->list #'prems) 
-                           'flatten #`(list (term/nts (#,@output-pats) #,nts)) 
+                           'flatten #`(list (vector jf-derivation-id (term/nts (#,@output-pats) #,nts)))
                            (syntax->list #'(names ...))
                            (syntax->list #'(names/ellipses ...))
-                           #f)))
+                           #f
+                           #'jf-derivation-id)))
            (with-syntax ([(compiled-lhs compiled-input-ctcs compiled-output-ctcs)
                           (generate-temporaries '(compiled-lhs compiled-input-ctcs compiled-output-ctcs))])
              
              #`(
                 ;; pieces of a 'let' expression to be combined: first some bindings
-                ([compiled-lhs (compile-pattern lang `lhs #t)]
+                ([jf-derivation-id '()]
+                 [compiled-lhs (compile-pattern lang `lhs #t)]
                  #,@(if (contracts-compilation input-contracts) 
                         (list #`[compiled-input-ctcs #,(contracts-compilation input-contracts)])
                         (list))
@@ -574,8 +636,8 @@
                   (combine-judgment-rhses
                    compiled-lhs
                    input
-                   (λ (m)
-                     (term-let ([names/ellipses (lookup-binding (mtch-bindings m) 'names)] ...)
+                   (λ (bnds)
+                     (term-let ([names/ellipses (lookup-binding bnds 'names)] ...)
                                #,body))
                    #,(if (contracts-compilation output-contracts)
                          #`(λ (output)
@@ -614,7 +676,7 @@
     [mtchs
      (define output-table (make-hash))
      (for ([m (in-list mtchs)])
-       (define os (rhs m))
+       (define os (rhs (mtch-bindings m)))
        (when os
          (for ([x (in-list os)])
            (hash-set! output-table x #t))))
@@ -634,7 +696,10 @@
            [no-rhss (map (λ (_) '()) clauses)])
        #`(generate-lws #t (conc-body ...) #,(lhs-lws clauses) #,rev-premss #,no-rhss #f))]))
 
-(define (check-judgment-form-contract form-name terms contracts mode modes)
+(define (check-judgment-form-contract form-name term+trees contracts mode modes)
+  (define terms (if (eq? mode 'O)
+                    (vector-ref term+trees 1)
+                    term+trees))
   (define description
     (case mode
       [(I) "input"]
@@ -1123,7 +1188,9 @@
 (provide define-judgment-form 
          define-extended-judgment-form
          judgment-holds
+         build-derivations
          generate-lws
+         (struct-out derivation)
          (for-syntax extract-term-let-binds
                      name-pattern-lws
                      extract-pattern-binds
diff --git a/collects/redex/private/matcher.rkt b/collects/redex/private/matcher.rkt
index 1e9fd47a48..b0124b05dd 100644
--- a/collects/redex/private/matcher.rkt
+++ b/collects/redex/private/matcher.rkt
@@ -997,11 +997,12 @@ See match-a-pattern.rkt for more details
     (error 'convert-matcher 
            "not a unary proc: ~s" 
            boolean-based-matcher))
-  (λ (exp hole-info)
+  (define (match-boolean-to-record-converter exp hole-info)
     (and (boolean-based-matcher exp)
          (list (make-mtch empty-bindings
                           (build-flat-context exp)
-                          none)))))
+                          none))))
+  match-boolean-to-record-converter)
 
 ;; match-named-pat : symbol <compiled-pattern> -> <compiled-pattern>
 (define (match-named-pat name match-pat mismatch-bind?)
diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt
index 22ac232524..5649703c66 100644
--- a/collects/redex/private/reduction-semantics.rkt
+++ b/collects/redex/private/reduction-semantics.rkt
@@ -726,7 +726,8 @@
                                         (term #,to #:lang #,lang)))
                           (syntax->list #'(names ...))
                           (syntax->list #'(names/ellipses ...))
-                          #t))
+                          #t
+                          #f))
             (define test-case-body-code
               ;; this contains some redundant code
               (bind-withs orig-name
@@ -738,7 +739,8 @@
                           #'#t
                           (syntax->list #'(names ...))
                           (syntax->list #'(names/ellipses ...))
-                          #t))
+                          #t
+                          #f))
             (with-syntax ([(lhs-w/extras (w/extras-names ...) (w/extras-names/ellipses ...))
                            (rw-sc #`(side-condition #,from #,test-case-body-code))]
                           [lhs-source (format "~a:~a:~a"
@@ -1232,7 +1234,8 @@
                                     #`(list (term #,rhs #:lang lang))
                                     (syntax->list names) 
                                     (syntax->list names/ellipses)
-                                    #t))
+                                    #t
+                                    #f))
                                  (syntax->list #'((stuff ...) ...))
                                  (syntax->list #'(rhs ...))
                                  (syntax->list #'(lhs-names ...))
@@ -1246,7 +1249,8 @@
                                     #`#t
                                     (syntax->list names)
                                     (syntax->list names/ellipses)
-                                    #t))
+                                    #t
+                                    #f))
                                  (syntax->list #'((stuff ...) ...))
                                  (syntax->list #'(rhs ...))
                                  (syntax->list #'(lhs-names ...))
diff --git a/collects/redex/reduction-semantics.rkt b/collects/redex/reduction-semantics.rkt
index ea2e41dcfe..7fb73dae3b 100644
--- a/collects/redex/reduction-semantics.rkt
+++ b/collects/redex/reduction-semantics.rkt
@@ -35,6 +35,8 @@
          define-judgment-form
          define-extended-judgment-form
          judgment-holds
+         build-derivations
+         (struct-out derivation)
          in-domain?
          caching-enabled?
          make-coverage
diff --git a/collects/redex/scribblings/ref.scrbl b/collects/redex/scribblings/ref.scrbl
index 0b6a2c67e3..5fe9349420 100644
--- a/collects/redex/scribblings/ref.scrbl
+++ b/collects/redex/scribblings/ref.scrbl
@@ -1386,6 +1386,20 @@ each satisfying assignment of pattern variables.
 See @racket[define-judgment-form] for examples.
 }
 
+@defform[(build-derivations judgment)]{
+  Constructs all of the @racket[derivation] trees
+  for @racket[judgment]. 
+  
+@examples[
+#:eval redex-eval
+       (build-derivations (even (s (s z))))]
+}
+
+@defstruct[derivation ([term any/c] [subs (listof derivation?)])]{
+  Represents a derivation from a judgment form. See also
+  @racket[build-derivations].
+}
+                                                            
 @defidform[I]{
 Recognized specially within @racket[define-judgment-form], the @racket[I] keyword
 is an error elsewhere.
diff --git a/collects/redex/tests/tl-test.rkt b/collects/redex/tests/tl-test.rkt
index 51d2b131e0..47cc3c3e02 100644
--- a/collects/redex/tests/tl-test.rkt
+++ b/collects/redex/tests/tl-test.rkt
@@ -2335,6 +2335,92 @@
       (test (judgment-holds (J1 1 any) any) '(1))
       (test (judgment-holds (J2 1 any) any) '(1))
       (test (judgment-holds (J2 4 any) any) '(4)))
+    
+    (let ()
+      (define-language L (N ::= z (s N) (t N)))
+      
+      (define-judgment-form L
+        #:mode (J2 I O)
+        [--------
+         (J2 1 1)]
+        [--------
+         (J2 1 2)])
+      
+      (test (build-derivations (J2 1 any))
+            (list (derivation '(J2 1 1) '())
+                  (derivation '(J2 1 2) '())))
+      
+      
+      
+      (define-judgment-form L
+        #:contract (K any any)
+        #:mode (K I O)
+        [-----------
+         (K () z)]
+        [(K any_1 N) ...
+         ---------------------------
+         (K (any_1 ...) (N ...))])
+      
+      
+      
+      (test (build-derivations (K (()) any))
+            (list (derivation '(K (()) (z))
+                              (list (derivation '(K () z)
+                                                '())))))
+      
+      (test
+       (build-derivations (K (() ()) any))
+       (list (derivation 
+              '(K (() ()) (z z))
+              (list
+               (derivation '(K () z) '())
+               (derivation '(K () z) '())))))
+      
+      (define-judgment-form L
+        #:contract (J any any)
+        #:mode (J I O)
+        [--------
+         (J () z)]
+        [(J any_1 N)  (J any_2 N)
+                      ----------------------------
+                      (J (any_1 any_2) (s N))]
+        [(J any N)
+         ---------------
+         (J (any) (s N))])
+      
+      (test (build-derivations 
+             (J ((()) (())) N))
+            (list (derivation
+                   '(J ((()) (())) (s (s z)))
+                   (list (derivation 
+                          '(J (()) (s z))
+                          (list
+                           (derivation
+                            '(J () z)
+                            '())))
+                         (derivation 
+                          '(J (()) (s z))
+                          (list
+                           (derivation
+                            '(J () z)
+                            '())))))))
+      
+      (define-judgment-form L
+        #:mode (J3 I O)
+        [(J any_1 any_2)
+         ------------
+         (J3 any_1 any_2)])
+      
+      (test (build-derivations (J3 (()) N))
+            (list (derivation
+                   '(J3 (()) (s z))
+                   (list
+                    (derivation
+                     '(J (()) (s z))
+                     (list 
+                      (derivation 
+                       '(J () z)
+                       '()))))))))
 
     
     (parameterize ([current-namespace (make-base-namespace)])