diff --git a/collects/redex/private/judgment-form.rkt b/collects/redex/private/judgment-form.rkt
new file mode 100644
index 0000000000..75bca90ac7
--- /dev/null
+++ b/collects/redex/private/judgment-form.rkt
@@ -0,0 +1,804 @@
+#lang racket/base
+
+(require "matcher.rkt"
+         "term.rkt"
+         "fresh.rkt"
+         "error.rkt"
+         racket/trace)
+
+(require
+ (for-syntax "rewrite-side-conditions.rkt"
+             "term-fn.rkt"
+             "loc-wrapper-ct.rkt"
+             racket/base
+             racket/syntax
+             syntax/id-table
+             racket/list
+             syntax/parse))
+
+;; Intermediate structures recording clause "extras" for typesetting.
+(define-struct metafunc-extra-side-cond (expr))
+(define-struct metafunc-extra-where (lhs rhs))
+(define-struct metafunc-extra-fresh (vars))
+
+(define-for-syntax (prune-syntax stx)
+  (datum->syntax
+   (identifier-prune-lexical-context #'whatever '(#%app #%datum))
+   (let loop ([stx stx])
+     (syntax-case stx ()
+       [(a . b)
+        (datum->syntax (identifier-prune-lexical-context #'whatever '(#%app))
+                       (cons (loop #'a) (loop #'b))
+                       stx)]
+       [x 
+        (identifier? #'x)
+        (identifier-prune-lexical-context #'x (list (syntax-e #'x) '#%top))]
+       [() (datum->syntax #f '() stx)]
+       [_ (datum->syntax (identifier-prune-lexical-context #'whatever '(#%datum))
+                         (syntax->datum stx) stx)]))))
+
+(define-syntax (--> stx) (raise-syntax-error '--> "used outside of reduction-relation"))
+(define-syntax (fresh stx) (raise-syntax-error 'fresh "used outside of reduction-relation"))
+(define-syntax (with stx) (raise-syntax-error 'with "used outside of reduction-relation"))
+
+(define-for-syntax (generate-binding-constraints names names/ellipses bindings syn-err-name)
+  (define (id/depth stx)
+    (syntax-case stx ()
+      [(s (... ...))
+       (let ([r (id/depth #'s)])
+         (make-id/depth (id/depth-id r) (add1 (id/depth-depth r)) (id/depth-mismatch? r)))]
+      [s (make-id/depth #'s 0 #f)]))
+  (define temporaries (generate-temporaries names))
+  (values
+   (for/fold ([cs '()])
+     ([n names]
+      [w/e names/ellipses]
+      [x temporaries])
+     (cond [(hash-ref bindings (syntax-e n) #f)
+            => (λ (b) 
+                 (let ([b-id/depth (id/depth b)]
+                       [n-id/depth (id/depth w/e)])
+                   (if (= (id/depth-depth b-id/depth) (id/depth-depth n-id/depth))
+                       (cons #`(equal? #,x (term #,b)) cs)
+                       (raise-ellipsis-depth-error
+                        syn-err-name
+                        (id/depth-id n-id/depth) (id/depth-depth n-id/depth)
+                        (id/depth-id b-id/depth) (id/depth-depth b-id/depth)))))]
+           [else cs]))
+   temporaries
+   (for/fold ([extended bindings])
+     ([name names] 
+      [w/ellipses names/ellipses])
+     (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?)
+  (with-disappeared-uses
+   (let loop ([stx stx]
+              [to-not-be-in main]
+              [env (make-immutable-hash
+                    (map (λ (x e) (cons (syntax-e x) e))
+                         names w/ellipses))])
+     (syntax-case stx (fresh judgment-holds)
+       [() body]
+       [((-where x e) y ...)
+        (where-keyword? #'-where)
+        (let ()
+          (with-syntax ([(side-conditions-rewritten (names ...) (names/ellipses ...))
+                         (rewrite-side-conditions/check-errs
+                          lang-nts
+                          'reduction-relation
+                          #t
+                          #'x)])
+            (define-values (binding-constraints temporaries env+)
+              (generate-binding-constraints (syntax->list #'(names ...))
+                                            (syntax->list #'(names/ellipses ...))
+                                            env
+                                            orig-name))
+            (with-syntax ([(binding-constraints ...) binding-constraints]
+                          [(x ...) temporaries])
+              (define rest-body (loop #'(y ...) #`(list x ... #,to-not-be-in) env+))
+              #`(#,(case where-mode
+                     [(flatten)
+                      #'combine-where-results/flatten]
+                     [(predicate)
+                      #'combine-where-results/predicate]
+                     [else (error 'unknown-where-mode "~s" where-mode)])
+                 (match-pattern (compile-pattern #,lang `side-conditions-rewritten #t) (term e))
+                 (λ (bindings)
+                   (let ([x (lookup-binding bindings 'names)] ...)
+                     (and binding-constraints ...
+                          (term-let ([names/ellipses x] ...) 
+                                    #,rest-body))))))))]
+       [((-side-condition s ...) y ...)
+        (side-condition-keyword? #'-side-condition)
+        (if side-condition-unquoted?
+            #`(and s ... #,(loop #'(y ...) to-not-be-in env))
+            #`(and (term s) ... #,(loop #'(y ...) to-not-be-in env)))]
+       [((fresh x) y ...)
+        (identifier? #'x)
+        #`(term-let ([x (variable-not-in #,to-not-be-in 'x)]) 
+                    #,(loop #'(y ...) #`(list (term x) #,to-not-be-in) env))]
+       [((fresh x name) y ...)
+        (identifier? #'x)
+        #`(term-let ([x (let ([the-name (term name)])
+                          (verify-name-ok '#,orig-name the-name)
+                          (variable-not-in #,to-not-be-in the-name))])
+                    #,(loop #'(y ...) #`(list (term x) #,to-not-be-in) env))]
+       [((fresh (y) (x ...)) z ...)
+        #`(term-let ([(y #,'...)
+                      (variables-not-in #,to-not-be-in 
+                                        (map (λ (_ignore_) 'y)
+                                             (term (x ...))))])
+                    #,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in) env))]
+       [((fresh (y) (x ...) names) z ...)
+        #`(term-let ([(y #,'...)
+                      (let ([the-names (term names)]
+                            [len-counter (term (x ...))])
+                        (verify-names-ok '#,orig-name the-names len-counter)
+                        (variables-not-in #,to-not-be-in the-names))])
+                    #,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in) env))]
+       [((judgment-holds j) . after)
+        (loop (cons #'j #'after) to-not-be-in env)]
+       [((form-name . pats) . after)
+        (judgment-form-id? #'form-name)
+        (let*-values ([(premise) (syntax-case stx () [(p . _) #'p])]
+                      [(rest-clauses under-ellipsis?)
+                       (syntax-case #'after ()
+                         [(maybe-ellipsis . more)
+                          (ellipsis? #'maybe-ellipsis)
+                          (values #'more #t)]
+                         [_ (values #'after #f)])]
+                      [(judgment-form) (syntax-local-value/record #'form-name (λ (_) #t))]
+                      [(mode) (judgment-form-mode judgment-form)]
+                      [(judgment-proc) (judgment-form-proc judgment-form)]
+                      [(input-template output-pre-pattern) 
+                       (let-values ([(in out) (split-by-mode (syntax->list #'pats) mode)])
+                         (if under-ellipsis?
+                             (let ([ellipsis (syntax/loc premise (... ...))])
+                               (values #`(#,in #,ellipsis) #`(#,out #,ellipsis)))
+                             (values in out)))]
+                      [(output-pattern output-names output-names/ellipses)
+                       (with-syntax ([(output names names/ellipses)
+                                      (rewrite-side-conditions/check-errs lang-nts orig-name #t output-pre-pattern)])
+                         (values #'output
+                                 (syntax->list #'names)
+                                 (syntax->list #'names/ellipses)))]
+                      [(binding-constraints temporaries env+)
+                       (generate-binding-constraints output-names output-names/ellipses env orig-name)]
+                      [(rest-body) (loop rest-clauses #`(list judgment-output #,to-not-be-in) env+)]
+                      [(call)
+                       (let ([input (quasisyntax/loc premise (term #,input-template))])
+                         (define (make-traced input)
+                           (quasisyntax/loc premise
+                             (call-judgment-form 'form-name #,judgment-proc '#,mode #,input)))
+                         (if under-ellipsis?
+                             #`(repeated-premise-outputs #,input (λ (x) #,(make-traced #'x)))
+                             (make-traced input)))])
+          (with-syntax ([(output-name ...) output-names]
+                        [(output-name/ellipsis ...) output-names/ellipses]
+                        [(temp ...) temporaries]
+                        [(binding-constraint ...) binding-constraints])
+            #`(begin
+                (void #,(defined-check judgment-proc "judgment form" #:external #'form-name))
+                (for/fold ([outputs '()]) ([sub-output #,call])
+                  (define mtchs
+                    (match-pattern (compile-pattern #,lang `#,output-pattern #t) sub-output))
+                  (if mtchs
+                      (for/fold ([outputs outputs]) ([mtch mtchs])
+                        (let ([temp (lookup-binding (mtch-bindings mtch) 'output-name)] ...)
+                          (define mtch-outputs
+                            (and binding-constraint ...
+                                 (term-let ([output-name/ellipsis temp] ...) 
+                                           #,rest-body)))
+                          (if mtch-outputs
+                              (append mtch-outputs outputs)
+                              outputs)))
+                      outputs)))))]))))
+
+(define (combine-where-results/flatten mtchs result)
+  (and mtchs
+       (for/fold ([r '()]) ([m mtchs])
+         (let ([s (result (mtch-bindings m))])
+           (if s (append s r) r)))))
+
+(define (combine-where-results/predicate mtchs result)
+  (and mtchs 
+       (for/or ([mtch mtchs])
+         (result (mtch-bindings mtch)))))
+
+(define (repeated-premise-outputs inputs premise)
+  (if (null? inputs)
+      '(())
+      (let ([output (premise (car inputs))])
+        (if (null? output)
+            '()
+            (for*/list ([o output] [os (repeated-premise-outputs (cdr inputs) premise)])
+                       (cons o os))))))
+
+(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 (assemble inputs outputs)
+          (let loop ([ms mode] [is inputs] [os outputs])
+            (if (null? ms)
+                '()
+                (case (car ms)
+                  [(I) (cons (car is) (loop (cdr ms) (cdr is) os))]
+                  [(O) (cons (car os) (loop (cdr ms) is (cdr os)))]))))
+        (define (wrapped . _)
+          (set! outputs (form-proc input))
+          (for/list ([output outputs])
+            (cons form-name (assemble input output))))
+        (apply trace-call form-name wrapped (assemble input spacers))
+        outputs)
+      (form-proc input)))
+
+(define (verify-name-ok orig-name the-name)
+  (unless (symbol? the-name)
+    (error orig-name "expected a single name, got ~s" the-name)))
+
+(define (verify-names-ok orig-name the-names len-counter)
+  (unless (and (list? the-names)
+               (andmap symbol? the-names))
+    (error orig-name
+           "expected a sequence of names, got ~s"
+           the-names))
+  (unless (= (length len-counter)
+             (length the-names))
+    (error orig-name
+           "expected the length of the sequence of names to be ~a, got ~s"
+           (length len-counter)
+           the-names)))
+
+(define current-traced-metafunctions (make-parameter '()))
+
+(define-for-syntax (mode-keyword stx)
+  (raise-syntax-error #f "keyword invalid outside of mode specification" stx))
+(define-syntax I mode-keyword)
+(define-syntax O mode-keyword)
+
+(define-for-syntax (check-judgment-arity stx judgment)
+  (syntax-case judgment ()
+    [(form-name pat ...)
+     (judgment-form-id? #'form-name)
+     (let ([expected (length (judgment-form-mode (syntax-local-value #'form-name)))]
+           [actual (length (syntax->list #'(pat ...)))])
+       (unless (= actual expected)
+         (raise-syntax-error 
+          #f 
+          (format "mode specifies a ~a-ary relation but use supplied ~a term~a" 
+                  expected actual (if (= actual 1) "" "s"))
+          judgment)))]
+    [(form-name pat ...)
+     (raise-syntax-error #f "expected a judgment form name" stx #'form-name)]))
+
+(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-for-syntax (definition-nts lang orig-stx syn-error-name)
+  (unless (identifier? lang)
+    (raise-syntax-error #f "expected an identifier in the language position" orig-stx lang))
+  (language-id-nts lang syn-error-name))
+
+(define-for-syntax (lhs-lws clauses)
+  (with-syntax ([((lhs-for-lw _ ...) ...) clauses])
+    (map (λ (x) (to-lw/proc (datum->syntax #f (cdr (syntax-e x)) x)))
+         (syntax->list #'(lhs-for-lw ...)))))
+
+(define-syntax (define-judgment-form stx)
+  (not-expression-context stx)
+  (syntax-case stx ()
+    [(def-form-id lang . body)
+     (let ([lang #'lang]
+           [syn-err-name (syntax-e #'def-form-id)])
+       (define nts (definition-nts lang stx syn-err-name))
+       (define-values (judgment-form-name dup-form-names mode position-contracts clauses)
+         (parse-judgment-form-body #'body syn-err-name stx))
+       (define definitions
+         #`(begin
+             (define-syntax #,judgment-form-name 
+               (judgment-form '#,judgment-form-name '#,mode #'judgment-form-proc #'#,lang #'judgment-form-lws))
+             (define judgment-form-proc
+               (compile-judgment-form-proc #,judgment-form-name #,lang #,mode #,clauses #,position-contracts #,stx #,syn-err-name))
+             (define judgment-form-lws
+               (compiled-judgment-form-lws #,clauses))))
+       (syntax-property
+        (prune-syntax
+         (if (eq? 'top-level (syntax-local-context))
+             ; Introduce the names before using them, to allow
+             ; judgment form definition at the top-level.
+             #`(begin 
+                 (define-syntaxes (judgment-form-proc judgment-form-lws) (values))
+                 #,definitions)
+             definitions))
+        'disappeared-use
+        (map syntax-local-introduce dup-form-names)))]))
+
+(define-for-syntax (parse-judgment-form-body body syn-err-name full-stx)
+  (define-syntax-class pos-mode
+    #:literals (I O)
+    (pattern I)
+    (pattern O))
+  (define-syntax-class mode-spec
+    #:description "mode specification"
+    (pattern (_:id _:pos-mode ...)))
+  (define-syntax-class contract-spec
+    #:description "contract specification"
+    (pattern (_:id _:expr ...)))
+  (define (horizontal-line? id)
+    (regexp-match? #rx"^-+$" (symbol->string (syntax-e id))))
+  (define-syntax-class horizontal-line
+    (pattern x:id #:when (horizontal-line? #'x)))
+  (define (parse-rules rules)
+    (for/list ([rule rules])
+      (syntax-parse rule
+        [(prem ... _:horizontal-line conc)
+         #'(conc prem ...)]
+        [_ rule])))
+  (define-values (name/mode mode name/contract contract rules)
+    (syntax-parse body #:context full-stx
+      [((~or (~seq #:mode ~! mode:mode-spec)
+             (~seq #:contract ~! contract:contract-spec))
+        ...
+        rule:expr ...)
+       (let-values ([(name/mode mode)
+                     (syntax-parse #'(mode ...)
+                       [((name . mode)) (values #'name (syntax->list #'mode))]
+                       [_ (raise-syntax-error 
+                           #f "expected definition to include a mode specification"
+                           full-stx)])]
+                    [(name/ctc ctc)
+                     (syntax-parse #'(contract ...)
+                       [() (values #f #f)]
+                       [((name . contract)) (values #'name (syntax->list #'contract))]
+                       [(_ . dups)
+                        (raise-syntax-error 
+                         syn-err-name "expected at most one contract specification"
+                         #f #f (syntax->list #'dups))])])
+         (values name/mode mode name/ctc ctc
+                 (parse-rules (syntax->list #'(rule ...)))))]))
+  (check-clauses full-stx syn-err-name rules #t)
+  (check-arity-consistency mode contract full-stx)
+  (define-values (form-name dup-names)
+    (syntax-case rules ()
+      [() (raise-syntax-error #f "expected at least one rule" full-stx)]
+      [_ (defined-name (list name/mode name/contract) rules full-stx)]))
+  (values form-name dup-names mode contract rules))
+
+(define-for-syntax (check-arity-consistency mode contracts full-def)
+  (when (and contracts (not (= (length mode) (length contracts))))
+    (raise-syntax-error 
+     #f "mode and contract specify different numbers of positions" full-def)))
+
+(define-for-syntax (defined-name declared-names clauses orig-stx)
+  (with-syntax ([(((used-names _ ...) _ ...) ...) clauses])
+    (define-values (the-name other-names)
+      (let ([present (filter values declared-names)])
+        (if (null? present)
+            (values (car (syntax->list #'(used-names ...)))
+                    (cdr (syntax->list #'(used-names ...))))
+            (values (car present) 
+                    (append (cdr present) (syntax->list #'(used-names ...)))))))
+    (let loop ([others other-names])
+      (cond
+        [(null? others) (values the-name other-names)]
+        [else
+         (unless (eq? (syntax-e the-name) (syntax-e (car others)))
+           (raise-syntax-error 
+            #f
+            "expected the same name in both positions"
+            orig-stx
+            the-name (list (car others))))
+         (loop (cdr others))]))))
+
+(define-syntax (judgment-holds stx)
+  (syntax-case stx ()
+    [(j-h judgment)
+     #`(not (null? #,(syntax/loc stx (j-h judgment #t))))]
+    [(j-h (form-name . pats) tmpl)
+     (judgment-form-id? #'form-name)
+     (let* ([syn-err-name (syntax-e #'j-h)]
+            [lang (judgment-form-lang (syntax-local-value #'form-name))]
+            [nts (definition-nts lang stx syn-err-name)]
+            [judgment (syntax-case stx () [(_ judgment _) #'judgment])])
+       (check-judgment-arity stx judgment)
+       #`(sort #,(bind-withs syn-err-name '() lang nts (list judgment)
+                             'flatten #`(list (term #,#'tmpl)) '() '() #f)
+               string<=?
+               #:key (λ (x) (format "~s" x))))]
+    [(_ (not-form-name . _) . _)
+     (not (judgment-form-id? #'form-name))
+     (raise-syntax-error #f "expected a judgment form name" stx #'not-form-name)]))
+
+(define-for-syntax (do-compile-judgment-form-proc name mode clauses contracts nts lang syn-error-name)
+  (define (compile-clause clause)
+    (syntax-case clause ()
+      [((_ . conc-pats) . prems)
+       (let-values ([(input-pats output-pats) (split-by-mode (syntax->list #'conc-pats) mode)])
+         (define ((rewrite-pattern binds?) pat)
+           (rewrite-side-conditions/check-errs nts syn-error-name binds? pat))
+         (with-syntax ([(lhs (names ...) (names/ellipses ...)) ((rewrite-pattern #t) input-pats)])
+           (define (contracts-compilation ctcs)
+             (and ctcs
+                  (with-syntax ([(ctc ...) ctcs])
+                    #`(list (compile-pattern #,lang `ctc #f) ...))))
+           (define-values (input-contracts output-contracts)
+             (syntax-case contracts ()
+               [#f (values #f #f)]
+               [(p ...) 
+                (let-values ([(ins outs) (split-by-mode (syntax->list #'(p ...)) mode)])
+                  (with-syntax ([((in-pat in-names in-names/ellipses) ...)
+                                 (map (rewrite-pattern #f) ins)]
+                                [((out-pat out-names out-names/ellipses) ...)
+                                 (map (rewrite-pattern #f) outs)])
+                  (values #'(in-pat ...)
+                          #'(out-pat ...))))]))
+           (define body
+             (bind-withs syn-error-name '() lang nts (syntax->list #'prems) 
+                         'flatten #`(list (term (#,@output-pats))) 
+                         (syntax->list #'(names ...))
+                         (syntax->list #'(names/ellipses ...))
+                         #f))
+           #`(let ([compiled-lhs (compile-pattern #,lang `lhs #t)]
+                   [compiled-input-ctcs #,(contracts-compilation input-contracts)]
+                   [compiled-output-ctcs #,(contracts-compilation output-contracts)])
+               (λ (input)
+                 (check-judgment-form-contract `#,name input compiled-input-ctcs 'I '#,mode)
+                 (combine-judgment-rhses
+                  compiled-lhs
+                  input
+                  (λ (m)
+                    (term-let ([names/ellipses (lookup-binding (mtch-bindings m) 'names)] ...)
+                              #,body))
+                  (λ (output)
+                    (check-judgment-form-contract `#,name output compiled-output-ctcs 'O '#,mode)))))))]))
+  (with-syntax ([(clause-proc ...) (map compile-clause clauses)]
+                [(clause-proc-ids ...) (generate-temporaries clauses)])
+    (with-syntax ([(backwards-ids ...) (reverse (syntax->list #'(clause-proc-ids ...)))])
+      #'(let ([clause-proc-ids clause-proc] ...)
+          (λ (input)
+            (append (backwards-ids input) ...))))))
+
+(define (combine-judgment-rhses compiled-lhs input rhs check-output)
+  (define mtchs (match-pattern compiled-lhs input))
+  (cond
+    [mtchs
+     (define output-table (make-hash))
+     (for ([m (in-list mtchs)])
+       (define os (rhs m))
+       (when os
+         (for ([x (in-list os)])
+           (hash-set! output-table x #t))))
+     (define outputs (hash-map output-table (λ (k v) k)))
+     (for ([output (in-list outputs)])
+       (check-output output))
+     outputs]
+    [else '()]))
+
+(define-for-syntax (do-compile-judgment-form-lws clauses)
+  (syntax-case clauses ()
+    [(((_ . conc-body) . prems) ...)
+     (let ([rev-premss
+            ; for consistency with metafunction extras
+            (for/list ([prems (syntax->list #'(prems ...))])
+              (reverse (syntax->list prems)))]
+           [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 description
+    (case mode
+      [(I) "input"]
+      [(O) "output"]))
+  (when contracts
+    (let loop ([rest-modes modes] [rest-terms terms] [rest-ctcs contracts] [pos 1])
+      (unless (null? rest-modes)
+        (if (eq? mode (car rest-modes))
+            (if (match-pattern (car rest-ctcs) (car rest-terms))
+                (loop (cdr rest-modes) (cdr rest-terms) (cdr rest-ctcs) (+ 1 pos))
+                (redex-error form-name "~a ~s at position ~s does not match its contract"
+                             description (car rest-terms) pos))
+            (loop (cdr rest-modes) rest-terms rest-ctcs (+ 1 pos)))))))
+
+(define-for-syntax (mode-check mode clauses nts syn-err-name orig-stx)
+  (define ((check-template bound-anywhere) temp bound)
+    (let check ([t temp])
+      (syntax-case t (unquote)
+        [(unquote . _)
+         (raise-syntax-error syn-err-name "unquote unsupported" t)]
+        [x
+         (identifier? #'x)
+         (unless (cond [(free-id-table-ref bound-anywhere #'x #f)
+                        (free-id-table-ref bound #'x #f)]
+                       [(id-binds? nts #t #'x)
+                        (term-fn? (syntax-local-value #'x (λ () #f)))]
+                       [else #t])
+           (raise-syntax-error syn-err-name "unbound pattern variable" #'x))]
+        [(u ...)
+         (for-each check (syntax->list #'(u ...)))]
+        [_ (void)])))
+  (define ((bind kind) pat bound)
+    (define-values (ids _)
+      (extract-names nts syn-err-name #t pat kind))
+    (for/fold ([b bound]) ([x ids])
+              (free-id-table-set b x #t)))
+  (define (split-body judgment)
+    (syntax-case judgment ()
+      [(form-name . body)
+       (split-by-mode (syntax->list #'body) (judgment-form-mode (syntax-local-value #'form-name)))]))
+  (define (drop-ellipses prems)
+    (syntax-case prems ()
+      [() '()]
+      [(prem maybe-ellipsis . remaining)
+       (ellipsis? #'maybe-ellipsis)
+       (syntax-case #'prem ()
+         [(form-name . _)
+          (judgment-form-id? #'form-name)
+          (cons #'prem (drop-ellipses #'remaining))]
+         [_ (raise-syntax-error syn-err-name "ellipses must follow judgment form uses" #'maybe-ellipsis)])]
+      [(prem . remaining)
+       (cons #'prem (drop-ellipses #'remaining))]))
+  (define (fold-clause pat-pos tmpl-pos acc-init clause)
+    (syntax-case clause ()
+      [(conc . prems)
+       (let-values ([(conc-in conc-out) (split-body #'conc)])
+         (check-judgment-arity orig-stx #'conc)
+         (define acc-out
+           (for/fold ([acc (foldl pat-pos acc-init conc-in)])
+                     ([prem (drop-ellipses #'prems)])
+                     (syntax-case prem ()
+                       [(-where pat tmpl)
+                        (where-keyword? #'-where)
+                        (begin
+                          (tmpl-pos #'tmpl acc)
+                          (pat-pos #'pat acc))]
+                       [(-side-condition tmpl)
+                        (side-condition-keyword? #'-side-condition)
+                        (begin (tmpl-pos #'tmpl acc)
+                               acc)]
+                       [(form-name . _)
+                        (if (judgment-form-id? #'form-name)
+                            (let-values ([(prem-in prem-out) (split-body prem)])
+                              (check-judgment-arity orig-stx prem)
+                              (for ([pos prem-in]) (tmpl-pos pos acc))
+                              (foldl pat-pos acc prem-out))
+                            (raise-syntax-error syn-err-name "expected judgment form name" #'form-name))]
+                       [_ (raise-syntax-error syn-err-name "malformed premise" prem)])))
+         (for ([pos conc-out]) (tmpl-pos pos acc-out))
+         acc-out)]))
+  (for ([clause clauses])
+    (define do-tmpl
+      (check-template
+       (fold-clause (bind 'rhs-only) void (make-immutable-free-id-table) clause)))
+    (fold-clause (bind 'rhs-only) do-tmpl (make-immutable-free-id-table) clause)))
+
+(define-syntax (generate-lws stx)
+  (syntax-case stx ()
+    [(_ relation? seq-of-lhs seq-of-lhs-for-lw seq-of-tl-side-cond/binds seq-of-rhs side-condition-unquoted?)
+     (with-syntax
+         ([(rhs/lw ...) 
+           (syntax-case #'relation? ()
+             [#t (map (λ (x) #`(list #,@(map to-lw/proc (syntax->list x))))
+                      (syntax->list #'seq-of-rhs))]
+             [#f (map to-lw/proc (syntax->list #'seq-of-rhs))])]
+          [(((bind-id/lw . bind-pat/lw) ...) ...)
+           ;; Also for pict, extract pattern bindings
+           (map name-pattern-lws (syntax->list #'seq-of-lhs))]
+          [((where/sc/lw ...) ...)
+           ;; Also for pict, extract where bindings
+           (map (λ (hm)
+                  (map
+                   (λ (lst)
+                     (syntax-case lst (unquote side-condition where)
+                       [(form-name . _)
+                        (judgment-form-id? #'form-name)
+                        #`(make-metafunc-extra-side-cond #,(to-lw/proc lst))]
+                       [(form-name . _)
+                        (judgment-form-id? #'form-name)
+                        #`(make-metafunc-extra-side-cond #,(to-lw/proc lst))]
+                       [(where pat (unquote (f _ _)))
+                        (and (or (identifier? #'pat)
+                                 (andmap identifier? (syntax->list #'pat)))
+                             (or (free-identifier=? #'f #'variable-not-in)
+                                 (free-identifier=? #'f #'variables-not-in)))
+                        (with-syntax ([(ids ...)
+                                       (map to-lw/proc
+                                            (if (identifier? #'pat)
+                                                (list #'pat)
+                                                (syntax->list #'pat)))])
+                          #`(make-metafunc-extra-fresh
+                             (list ids ...)))]
+                       [(where pat exp)
+                        #`(make-metafunc-extra-where
+                           #,(to-lw/proc #'pat) #,(to-lw/proc #'exp))]
+                       [(side-condition x)
+                        #`(make-metafunc-extra-side-cond
+                           #,(if (syntax-e #'side-condition-unquoted?)
+                                 (to-lw/uq/proc #'x)
+                                 (to-lw/proc #'x)))]
+                       [maybe-ellipsis
+                        (ellipsis? #'maybe-ellipsis)
+                        (to-lw/proc #'maybe-ellipsis)]))
+                   (visible-extras hm)))
+                (syntax->list #'seq-of-tl-side-cond/binds))]
+          [(((where-bind-id/lw . where-bind-pat/lw) ...) ...)
+           (map (λ (clauses)
+                  (for/fold ([binds '()]) ([clause (visible-extras clauses)])
+                            (syntax-case clause (where)
+                              [(form-name . pieces)
+                               (judgment-form-id? #'form-name)
+                               (let*-values ([(mode) (judgment-form-mode (syntax-local-value #'form-name))]
+                                             [(_ outs) (split-by-mode (syntax->list #'pieces) mode)])
+                                 (for/fold ([binds binds]) ([out outs])
+                                           (append (name-pattern-lws out) binds)))]
+                              [(where lhs rhs) (append (name-pattern-lws #'lhs) binds)]
+                              [_ binds])))
+                (syntax->list #'seq-of-tl-side-cond/binds))]
+          [(((rhs-bind-id/lw . rhs-bind-pat/lw/uq) ...) ...)
+           ;; Also for pict, extract pattern bindings
+           (map (λ (x) (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/uq/proc (cdr x))))
+                            (extract-term-let-binds x)))
+                (syntax->list #'seq-of-rhs))]
+          
+          [(x-lhs-for-lw ...) #'seq-of-lhs-for-lw])
+       #'(list (list x-lhs-for-lw
+                     (list (make-metafunc-extra-where bind-id/lw bind-pat/lw) ...
+                           (make-metafunc-extra-where where-bind-id/lw where-bind-pat/lw) ...
+                           (make-metafunc-extra-where rhs-bind-id/lw rhs-bind-pat/lw/uq) ...
+                           where/sc/lw ...)
+                     rhs/lw)
+               ...))]))
+
+(define-for-syntax (visible-extras extras)
+  (for/fold ([visible empty]) ([extra (syntax->list extras)])
+            (syntax-case extra (where/hidden
+                                side-condition/hidden
+                                judgment-holds)
+              [(where/hidden pat exp) visible]
+              [(side-condition/hidden x) visible]
+              [(judgment-holds judgment)
+               (cons #'judgment visible)]
+              [_ (cons extra visible)])))
+
+(define-syntax (compile-judgment-form-proc stx)
+  (syntax-case stx ()
+    [(_ judgment-form-name lang mode clauses ctcs full-def syn-err-name)
+     (let ([nts (definition-nts #'lang #'full-def (syntax-e #'syn-err-name))])
+       (mode-check (syntax->datum #'mode) (syntax->list #'clauses) nts (syntax-e #'syn-err-name) stx)
+       (do-compile-judgment-form-proc
+        (syntax-e #'judgment-form-name) 
+        (syntax->datum #'mode) 
+        (syntax->list #'clauses) 
+        #'ctcs
+        nts
+        #'lang 
+        (syntax-e #'syn-err-name)))]))
+
+(define-syntax (compiled-judgment-form-lws stx)
+  (syntax-case stx ()
+    [(_ clauses)
+     (do-compile-judgment-form-lws (syntax->list #'clauses))]))
+
+(define-for-syntax (extract-term-let-binds lhs)
+  (let loop ([lhs lhs])
+    (syntax-case* lhs (term-let) (lambda (a b) (eq? (syntax-e a) (syntax-e b)))
+      [(term-let ((x e1) ...) e2 ...)
+       (append (map cons
+                    (syntax->list #'(x ...))
+                    (syntax->list #'(e1 ...)))
+               (loop #'(e2 ...)))]
+      ;; FIXME: should follow the grammar of patterns!
+      [(a . b)
+       (append (loop #'a) (loop #'b))]
+      [_else null])))
+
+
+
+(define-for-syntax (name-pattern-lws pat)
+  (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/proc (cdr x))))
+       (extract-pattern-binds pat)))
+
+(define-for-syntax (extract-pattern-binds lhs)
+  (let loop ([lhs lhs])
+    (syntax-case* lhs (name) (lambda (a b) (eq? (syntax-e a) (syntax-e b)))
+      [(name id expr)
+       (identifier? #'id)
+       (cons (cons #'id #'expr) (loop #'expr))]
+      ;; FIXME: should follow the grammar of patterns!
+      [(a . b)
+       (append (loop #'a) (loop #'b))]
+      [_else null])))
+
+(define-for-syntax (check-clauses stx syn-error-name rest relation?)
+  (syntax-case rest ()
+    [([(lhs ...) roc1 roc2 ...] ...)
+     rest]
+    [([(lhs ...) rhs ...] ...)
+     (if relation?
+         rest
+         (begin
+           (for-each 
+            (λ (clause)
+              (syntax-case clause ()
+                [(a b) (void)]
+                [x (raise-syntax-error syn-error-name "expected a pattern and a right-hand side" stx clause)]))
+            rest)
+           (raise-syntax-error syn-error-name "error checking failed.3" stx)))]
+    [([x roc ...] ...)
+     (begin
+       (for-each 
+        (λ (x)
+          (syntax-case x ()
+            [(lhs ...) (void)]
+            [x (raise-syntax-error syn-error-name "expected a function prototype" stx #'x)]))
+        (syntax->list #'(x ...)))
+       (raise-syntax-error syn-error-name "error checking failed.1" stx))]
+    [(x ...)
+     (begin
+       (for-each 
+        (λ (x)
+          (syntax-case x ()
+            [(stuff stuff2 ...) (void)]
+            [x (raise-syntax-error syn-error-name "expected a clause" stx #'x)]))
+        (syntax->list #'(x ...)))
+       (raise-syntax-error syn-error-name "error checking failed.2" stx))]))
+
+(define-for-syntax (split-by-mode xs mode)
+  (for/fold ([ins '()] [outs '()])
+            ([x (reverse xs)]
+             [m (reverse mode)])
+    (case m
+      [(I) (values (cons x ins) outs)]
+      [(O) (values ins (cons x outs))]
+      [else (error 'split-by-mode "ack ~s" m)])))
+
+(define-for-syntax (ellipsis? stx)
+  (and (identifier? stx)
+       (free-identifier=? stx (quote-syntax ...))))
+
+
+(define-for-syntax (where-keyword? id)
+  (or (free-identifier=? id #'where)
+      (free-identifier=? id #'where/hidden)))
+(define-for-syntax (side-condition-keyword? id)
+  (or (free-identifier=? id #'side-condition)
+      (free-identifier=? id #'side-condition/hidden)))
+
+(provide define-judgment-form 
+         judgment-holds
+         generate-lws
+         (for-syntax extract-term-let-binds
+                     name-pattern-lws
+                     extract-pattern-binds
+                     check-clauses
+                     split-by-mode
+                     where-keyword?
+                     side-condition-keyword?
+                     ellipsis?
+                     visible-extras))
+
+
+(provide --> fresh with I O ;; macro keywords
+         (for-syntax prune-syntax
+                     side-condition-keyword?
+                     bind-withs
+                     split-by-mode)
+         current-traced-metafunctions
+         
+         (struct-out metafunc-extra-side-cond)
+         (struct-out metafunc-extra-where)
+         (struct-out metafunc-extra-fresh))
diff --git a/collects/redex/private/pict.rkt b/collects/redex/private/pict.rkt
index 49e406c9e4..fd8a1be3cb 100644
--- a/collects/redex/private/pict.rkt
+++ b/collects/redex/private/pict.rkt
@@ -9,6 +9,7 @@
          texpict/utils
          
          "reduction-semantics.rkt"
+         "judgment-form.rkt"
          "struct.rkt"
          "loc-wrapper.rkt"
          "matcher.rkt"
diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt
index 318db1833e..9bbdff9b66 100644
--- a/collects/redex/private/reduction-semantics.rkt
+++ b/collects/redex/private/reduction-semantics.rkt
@@ -6,6 +6,7 @@
          "fresh.rkt"
          "loc-wrapper.rkt"
          "error.rkt"
+         "judgment-form.rkt"
          (for-syntax "cycle-check.rkt"
                      setup/path-to-relative)
          racket/trace
@@ -22,8 +23,6 @@
                      syntax/id-table
                      racket/base
                      racket/list
-                     racket/match
-                     racket/syntax
                      syntax/parse
                      syntax/parse/experimental/contract
                      syntax/name))
@@ -31,22 +30,6 @@
 (define (language-nts lang)
   (hash-map (compiled-lang-ht lang) (λ (x y) x)))
 
-(define-for-syntax (prune-syntax stx)
-  (datum->syntax
-   (identifier-prune-lexical-context #'whatever '(#%app #%datum))
-   (let loop ([stx stx])
-     (syntax-case stx ()
-       [(a . b)
-        (datum->syntax (identifier-prune-lexical-context #'whatever '(#%app))
-                       (cons (loop #'a) (loop #'b))
-                       stx)]
-       [x 
-        (identifier? #'x)
-        (identifier-prune-lexical-context #'x (list (syntax-e #'x) '#%top))]
-       [() (datum->syntax #f '() stx)]
-       [_ (datum->syntax (identifier-prune-lexical-context #'whatever '(#%datum))
-                         (syntax->datum stx) stx)]))))
-
 (define-for-syntax (term-matcher orig-stx make-matcher)
   (syntax-case orig-stx ()
     [(form-name lang [pattern rhs] ...)
@@ -219,10 +202,6 @@
      (reduction-relation-lws red)
      `any)))
 
-(define-syntax (--> stx) (raise-syntax-error '--> "used outside of reduction-relation"))
-(define-syntax (fresh stx) (raise-syntax-error 'fresh "used outside of reduction-relation"))
-(define-syntax (with stx) (raise-syntax-error 'with "used outside of reduction-relation"))
-
 (define (apply-reduction-relation/tagged p v)
   (let loop ([procs (reduction-relation-procs p)]
              [acc '()])
@@ -235,30 +214,6 @@
 (define (apply-reduction-relation/tag-with-names p v) (map cdr (apply-reduction-relation/tagged p v)))
 (define (apply-reduction-relation p v) (map caddr (apply-reduction-relation/tagged p v)))
 
-(define-for-syntax (extract-pattern-binds lhs)
-  (let loop ([lhs lhs])
-    (syntax-case* lhs (name) (lambda (a b) (eq? (syntax-e a) (syntax-e b)))
-      [(name id expr)
-       (identifier? #'id)
-       (cons (cons #'id #'expr) (loop #'expr))]
-      ;; FIXME: should follow the grammar of patterns!
-      [(a . b)
-       (append (loop #'a) (loop #'b))]
-      [_else null])))
-
-(define-for-syntax (extract-term-let-binds lhs)
-  (let loop ([lhs lhs])
-    (syntax-case* lhs (term-let) (lambda (a b) (eq? (syntax-e a) (syntax-e b)))
-      [(term-let ((x e1) ...) e2 ...)
-       (append (map cons
-                    (syntax->list #'(x ...))
-                    (syntax->list #'(e1 ...)))
-               (loop #'(e2 ...)))]
-      ;; FIXME: should follow the grammar of patterns!
-      [(a . b)
-       (append (loop #'a) (loop #'b))]
-      [_else null])))
-
 (define-syntax (-reduction-relation stx)
   (syntax-case stx ()
     [(_ lang args ...)
@@ -271,21 +226,6 @@
      (with-syntax ([orig-stx stx])
        (syntax/loc stx (do-reduction-relation orig-stx extend-reduction-relation orig-reduction-relation #t lang args ...)))]))
 
-(define-for-syntax (where-keyword? id)
-  (or (free-identifier=? id #'where)
-      (free-identifier=? id #'where/hidden)))
-(define-for-syntax (side-condition-keyword? id)
-  (or (free-identifier=? id #'side-condition)
-      (free-identifier=? id #'side-condition/hidden)))
-
-(define-for-syntax (split-by-mode xs mode)
-  (for/fold ([ins '()] [outs '()])
-            ([x (reverse xs)]
-             [m (reverse mode)])
-            (match m
-              ['I (values (cons x ins) outs)]
-              ['O (values ins (cons x outs))])))
-
 (define-for-syntax (generate-binding-constraints names names/ellipses bindings syn-err-name)
   (define (id/depth stx)
     (syntax-case stx ()
@@ -316,181 +256,6 @@
       [w/ellipses names/ellipses])
      (hash-set extended (syntax-e name) w/ellipses))))
 
-(define-for-syntax (ellipsis? stx)
-  (and (identifier? stx)
-       (free-identifier=? stx (quote-syntax ...))))
-
-;; 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?)
-  (with-disappeared-uses
-   (let loop ([stx stx]
-              [to-not-be-in main]
-              [env (make-immutable-hash
-                    (map (λ (x e) (cons (syntax-e x) e))
-                         names w/ellipses))])
-     (syntax-case stx (fresh judgment-holds)
-       [() body]
-       [((-where x e) y ...)
-        (where-keyword? #'-where)
-        (let ()
-          (with-syntax ([(side-conditions-rewritten (names ...) (names/ellipses ...))
-                         (rewrite-side-conditions/check-errs
-                          lang-nts
-                          'reduction-relation
-                          #t
-                          #'x)])
-            (define-values (binding-constraints temporaries env+)
-              (generate-binding-constraints (syntax->list #'(names ...))
-                                            (syntax->list #'(names/ellipses ...))
-                                            env
-                                            orig-name))
-            (with-syntax ([(binding-constraints ...) binding-constraints]
-                          [(x ...) temporaries])
-              (define rest-body (loop #'(y ...) #`(list x ... #,to-not-be-in) env+))
-              #`(#,(case where-mode
-                     [(flatten)
-                      #'combine-where-results/flatten]
-                     [(predicate)
-                      #'combine-where-results/predicate]
-                     [else (error 'unknown-where-mode "~s" where-mode)])
-                 (match-pattern (compile-pattern #,lang `side-conditions-rewritten #t) (term e))
-                 (λ (bindings)
-                   (let ([x (lookup-binding bindings 'names)] ...)
-                     (and binding-constraints ...
-                          (term-let ([names/ellipses x] ...) 
-                                    #,rest-body))))))))]
-       [((-side-condition s ...) y ...)
-        (side-condition-keyword? #'-side-condition)
-        (if side-condition-unquoted?
-            #`(and s ... #,(loop #'(y ...) to-not-be-in env))
-            #`(and (term s) ... #,(loop #'(y ...) to-not-be-in env)))]
-       [((fresh x) y ...)
-        (identifier? #'x)
-        #`(term-let ([x (variable-not-in #,to-not-be-in 'x)]) 
-                    #,(loop #'(y ...) #`(list (term x) #,to-not-be-in) env))]
-       [((fresh x name) y ...)
-        (identifier? #'x)
-        #`(term-let ([x (let ([the-name (term name)])
-                          (verify-name-ok '#,orig-name the-name)
-                          (variable-not-in #,to-not-be-in the-name))])
-                    #,(loop #'(y ...) #`(list (term x) #,to-not-be-in) env))]
-       [((fresh (y) (x ...)) z ...)
-        #`(term-let ([(y #,'...)
-                      (variables-not-in #,to-not-be-in 
-                                        (map (λ (_ignore_) 'y)
-                                             (term (x ...))))])
-                    #,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in) env))]
-       [((fresh (y) (x ...) names) z ...)
-        #`(term-let ([(y #,'...)
-                      (let ([the-names (term names)]
-                            [len-counter (term (x ...))])
-                        (verify-names-ok '#,orig-name the-names len-counter)
-                        (variables-not-in #,to-not-be-in the-names))])
-                    #,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in) env))]
-       [((judgment-holds j) . after)
-        (loop (cons #'j #'after) to-not-be-in env)]
-       [((form-name . pats) . after)
-        (judgment-form-id? #'form-name)
-        (let*-values ([(premise) (syntax-case stx () [(p . _) #'p])]
-                      [(rest-clauses under-ellipsis?)
-                       (syntax-case #'after ()
-                         [(maybe-ellipsis . more)
-                          (ellipsis? #'maybe-ellipsis)
-                          (values #'more #t)]
-                         [_ (values #'after #f)])]
-                      [(judgment-form) (syntax-local-value/record #'form-name (λ (_) #t))]
-                      [(mode) (judgment-form-mode judgment-form)]
-                      [(judgment-proc) (judgment-form-proc judgment-form)]
-                      [(input-template output-pre-pattern) 
-                       (let-values ([(in out) (split-by-mode (syntax->list #'pats) mode)])
-                         (if under-ellipsis?
-                             (let ([ellipsis (syntax/loc premise (... ...))])
-                               (values #`(#,in #,ellipsis) #`(#,out #,ellipsis)))
-                             (values in out)))]
-                      [(output-pattern output-names output-names/ellipses)
-                       (with-syntax ([(output names names/ellipses)
-                                      (rewrite-side-conditions/check-errs lang-nts orig-name #t output-pre-pattern)])
-                         (values #'output
-                                 (syntax->list #'names)
-                                 (syntax->list #'names/ellipses)))]
-                      [(binding-constraints temporaries env+)
-                       (generate-binding-constraints output-names output-names/ellipses env orig-name)]
-                      [(rest-body) (loop rest-clauses #`(list judgment-output #,to-not-be-in) env+)]
-                      [(call)
-                       (let ([input (quasisyntax/loc premise (term #,input-template))])
-                         (define (make-traced input)
-                           (quasisyntax/loc premise
-                             (call-judgment-form 'form-name #,judgment-proc '#,mode #,input)))
-                         (if under-ellipsis?
-                             #`(repeated-premise-outputs #,input (λ (x) #,(make-traced #'x)))
-                             (make-traced input)))])
-          (with-syntax ([(output-name ...) output-names]
-                        [(output-name/ellipsis ...) output-names/ellipses]
-                        [(temp ...) temporaries]
-                        [(binding-constraint ...) binding-constraints])
-            #`(begin
-                (void #,(defined-check judgment-proc "judgment form" #:external #'form-name))
-                (for/fold ([outputs '()]) ([sub-output #,call])
-                  (define mtchs
-                    (match-pattern (compile-pattern #,lang `#,output-pattern #t) sub-output))
-                  (if mtchs
-                      (for/fold ([outputs outputs]) ([mtch mtchs])
-                        (let ([temp (lookup-binding (mtch-bindings mtch) 'output-name)] ...)
-                          (define mtch-outputs
-                            (and binding-constraint ...
-                                 (term-let ([output-name/ellipsis temp] ...) 
-                                           #,rest-body)))
-                          (if mtch-outputs
-                              (append mtch-outputs outputs)
-                              outputs)))
-                      outputs)))))]))))
-
-(define (combine-where-results/flatten mtchs result)
-  (and mtchs
-       (for/fold ([r '()]) ([m mtchs])
-         (let ([s (result (mtch-bindings m))])
-           (if s (append s r) r)))))
-
-(define (combine-where-results/predicate mtchs result)
-  (and mtchs 
-       (for/or ([mtch mtchs])
-         (result (mtch-bindings mtch)))))
-
-(define (repeated-premise-outputs inputs premise)
-  (if (null? inputs)
-      '(())
-      (let ([output (premise (car inputs))])
-        (if (null? output)
-            '()
-            (for*/list ([o output] [os (repeated-premise-outputs (cdr inputs) premise)])
-                       (cons o os))))))
-
-(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 (assemble inputs outputs)
-          (let loop ([ms mode] [is inputs] [os outputs])
-            (if (null? ms)
-                '()
-                (case (car ms)
-                  [(I) (cons (car is) (loop (cdr ms) (cdr is) os))]
-                  [(O) (cons (car os) (loop (cdr ms) is (cdr os)))]))))
-        (define (wrapped . _)
-          (set! outputs (form-proc input))
-          (for/list ([output outputs])
-            (cons form-name (assemble input output))))
-        (apply trace-call form-name wrapped (assemble input spacers))
-        outputs)
-      (form-proc input)))
-
-(define-for-syntax (name-pattern-lws pat)
-  (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/proc (cdr x))))
-       (extract-pattern-binds pat)))
-
 (define-for-syntax (check-judgment-arity stx judgment)
   (syntax-case judgment ()
     [(form-name pat ...)
@@ -608,8 +373,9 @@
   
   (define (name-pattern-lws/rr pat)
     (for/list ([lw-pair (name-pattern-lws pat)])
-      (match lw-pair
-        [(cons l r) #`(cons #,l #,r)])))
+      (if (pair? lw-pair)
+          #`(cons #,(car lw-pair) #,(cdr lw-pair))
+          (error 'name-pattern-lws/rr "ack"))))
   
   (define (rule->lws rule)
     (syntax-case rule ()
@@ -1149,35 +915,6 @@
      lhs-source
      case-id)))
 
-(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)))
-
-(define (verify-names-ok orig-name the-names len-counter)
-  (unless (and (list? the-names)
-               (andmap symbol? the-names))
-    (error orig-name
-           "expected a sequence of names, got ~s"
-           the-names))
-  (unless (= (length len-counter)
-             (length the-names))
-    (error orig-name
-           "expected the length of the sequence of names to be ~a, got ~s"
-           (length len-counter)
-           the-names)))
-
 (define (union-reduction-relations fst snd . rst)
   (let ([name-ht (make-hasheq)]
         [counter 0]
@@ -1335,11 +1072,6 @@
 
 (define-struct metafunc-case (lhs rhs lhs+ src-loc id))
 
-;; Intermediate structures recording clause "extras" for typesetting.
-(define-struct metafunc-extra-side-cond (expr))
-(define-struct metafunc-extra-where (lhs rhs))
-(define-struct metafunc-extra-fresh (vars))
-
 (define-syntax (in-domain? stx)
   (syntax-case stx ()
     [(_ (name exp ...))
@@ -1620,85 +1352,7 @@
                   (map syntax-local-introduce 
                        (syntax->list #'(original-names ...))))))))))]))
 
-(define-syntax (define-judgment-form stx)
-  (not-expression-context stx)
-  (syntax-case stx ()
-    [(def-form-id lang . body)
-     (let ([lang #'lang]
-           [syn-err-name (syntax-e #'def-form-id)])
-       (define nts (definition-nts lang stx syn-err-name))
-       (define-values (judgment-form-name dup-form-names mode position-contracts clauses)
-         (parse-judgment-form-body #'body syn-err-name stx))
-       (define definitions
-         #`(begin
-             (define-syntax #,judgment-form-name 
-               (judgment-form '#,judgment-form-name '#,mode #'judgment-form-proc #'#,lang #'judgment-form-lws))
-             (define judgment-form-proc
-               (compile-judgment-form-proc #,judgment-form-name #,lang #,mode #,clauses #,position-contracts #,stx #,syn-err-name))
-             (define judgment-form-lws
-               (compiled-judgment-form-lws #,clauses))))
-       (syntax-property
-        (prune-syntax
-         (if (eq? 'top-level (syntax-local-context))
-             ; Introduce the names before using them, to allow
-             ; judgment form definition at the top-level.
-             #`(begin 
-                 (define-syntaxes (judgment-form-proc judgment-form-lws) (values))
-                 #,definitions)
-             definitions))
-        'disappeared-use
-        (map syntax-local-introduce dup-form-names)))]))
 
-(define-for-syntax (parse-judgment-form-body body syn-err-name full-stx)
-  (define-syntax-class pos-mode
-    #:literals (I O)
-    (pattern I)
-    (pattern O))
-  (define-syntax-class mode-spec
-    #:description "mode specification"
-    (pattern (_:id _:pos-mode ...)))
-  (define-syntax-class contract-spec
-    #:description "contract specification"
-    (pattern (_:id _:expr ...)))
-  (define (horizontal-line? id)
-    (regexp-match? #rx"^-+$" (symbol->string (syntax-e id))))
-  (define-syntax-class horizontal-line
-    (pattern x:id #:when (horizontal-line? #'x)))
-  (define (parse-rules rules)
-    (for/list ([rule rules])
-      (syntax-parse rule
-        [(prem ... _:horizontal-line conc)
-         #'(conc prem ...)]
-        [_ rule])))
-  (define-values (name/mode mode name/contract contract rules)
-    (syntax-parse body #:context full-stx
-      [((~or (~seq #:mode ~! mode:mode-spec)
-             (~seq #:contract ~! contract:contract-spec))
-        ...
-        rule:expr ...)
-       (let-values ([(name/mode mode)
-                     (syntax-parse #'(mode ...)
-                       [((name . mode)) (values #'name (syntax->list #'mode))]
-                       [_ (raise-syntax-error 
-                           #f "expected definition to include a mode specification"
-                           full-stx)])]
-                    [(name/ctc ctc)
-                     (syntax-parse #'(contract ...)
-                       [() (values #f #f)]
-                       [((name . contract)) (values #'name (syntax->list #'contract))]
-                       [(_ . dups)
-                        (raise-syntax-error 
-                         syn-err-name "expected at most one contract specification"
-                         #f #f (syntax->list #'dups))])])
-         (values name/mode mode name/ctc ctc
-                 (parse-rules (syntax->list #'(rule ...)))))]))
-  (check-clauses full-stx syn-err-name rules #t)
-  (check-arity-consistency mode contract full-stx)
-  (define-values (form-name dup-names)
-    (syntax-case rules ()
-      [() (raise-syntax-error #f "expected at least one rule" full-stx)]
-      [_ (defined-name (list name/mode name/contract) rules full-stx)]))
-  (values form-name dup-names mode contract rules))
 
 (define-for-syntax (check-arity-consistency mode contracts full-def)
   (when (and contracts (not (= (length mode) (length contracts))))
@@ -1788,40 +1442,6 @@
          stx
          rest)])]))
 
-(define-for-syntax (check-clauses stx syn-error-name rest relation?)
-  (syntax-case rest ()
-    [([(lhs ...) roc1 roc2 ...] ...)
-     rest]
-    [([(lhs ...) rhs ...] ...)
-     (if relation?
-         rest
-         (begin
-           (for-each 
-            (λ (clause)
-              (syntax-case clause ()
-                [(a b) (void)]
-                [x (raise-syntax-error syn-error-name "expected a pattern and a right-hand side" stx clause)]))
-            rest)
-           (raise-syntax-error syn-error-name "error checking failed.3" stx)))]
-    [([x roc ...] ...)
-     (begin
-       (for-each 
-        (λ (x)
-          (syntax-case x ()
-            [(lhs ...) (void)]
-            [x (raise-syntax-error syn-error-name "expected a function prototype" stx #'x)]))
-        (syntax->list #'(x ...)))
-       (raise-syntax-error syn-error-name "error checking failed.1" stx))]
-    [(x ...)
-     (begin
-       (for-each 
-        (λ (x)
-          (syntax-case x ()
-            [(stuff stuff2 ...) (void)]
-            [x (raise-syntax-error syn-error-name "expected a clause" stx #'x)]))
-        (syntax->list #'(x ...)))
-       (raise-syntax-error syn-error-name "error checking failed.2" stx))]))
-
 (define-for-syntax (parse-extras extras)
   (for-each
    (λ (stuffs)
@@ -1882,294 +1502,6 @@
                   (cons (cadr more) arg-pats))]
            [else (values (reverse arg-pats) more)])))]))
 
-(define-syntax (judgment-holds stx)
-  (syntax-case stx ()
-    [(j-h judgment)
-     #`(not (null? #,(syntax/loc stx (j-h judgment #t))))]
-    [(j-h (form-name . pats) tmpl)
-     (judgment-form-id? #'form-name)
-     (let* ([syn-err-name (syntax-e #'j-h)]
-            [lang (judgment-form-lang (syntax-local-value #'form-name))]
-            [nts (definition-nts lang stx syn-err-name)]
-            [judgment (syntax-case stx () [(_ judgment _) #'judgment])])
-       (check-judgment-arity stx judgment)
-       #`(sort #,(bind-withs syn-err-name '() lang nts (list judgment)
-                             'flatten #`(list (term #,#'tmpl)) '() '() #f)
-               string<=?
-               #:key (λ (x) (format "~s" x))))]
-    [(_ (not-form-name . _) . _)
-     (not (judgment-form-id? #'form-name))
-     (raise-syntax-error #f "expected a judgment form name" stx #'not-form-name)]))
-
-(define-for-syntax (do-compile-judgment-form-proc name mode clauses contracts nts lang syn-error-name)
-  (define (compile-clause clause)
-    (syntax-case clause ()
-      [((_ . conc-pats) . prems)
-       (let-values ([(input-pats output-pats) (split-by-mode (syntax->list #'conc-pats) mode)])
-         (define ((rewrite-pattern binds?) pat)
-           (rewrite-side-conditions/check-errs nts syn-error-name binds? pat))
-         (with-syntax ([(lhs (names ...) (names/ellipses ...)) ((rewrite-pattern #t) input-pats)])
-           (define (contracts-compilation ctcs)
-             (and ctcs
-                  (with-syntax ([(ctc ...) ctcs])
-                    #`(list (compile-pattern #,lang `ctc #f) ...))))
-           (define-values (input-contracts output-contracts)
-             (syntax-case contracts ()
-               [#f (values #f #f)]
-               [(p ...) 
-                (let-values ([(ins outs) (split-by-mode (syntax->list #'(p ...)) mode)])
-                  (with-syntax ([((in-pat in-names in-names/ellipses) ...)
-                                 (map (rewrite-pattern #f) ins)]
-                                [((out-pat out-names out-names/ellipses) ...)
-                                 (map (rewrite-pattern #f) outs)])
-                  (values #'(in-pat ...)
-                          #'(out-pat ...))))]))
-           (define body
-             (bind-withs syn-error-name '() lang nts (syntax->list #'prems) 
-                         'flatten #`(list (term (#,@output-pats))) 
-                         (syntax->list #'(names ...))
-                         (syntax->list #'(names/ellipses ...))
-                         #f))
-           #`(let ([compiled-lhs (compile-pattern #,lang `lhs #t)]
-                   [compiled-input-ctcs #,(contracts-compilation input-contracts)]
-                   [compiled-output-ctcs #,(contracts-compilation output-contracts)])
-               (λ (input)
-                 (check-judgment-form-contract `#,name input compiled-input-ctcs 'I '#,mode)
-                 (combine-judgment-rhses
-                  compiled-lhs
-                  input
-                  (λ (m)
-                    (term-let ([names/ellipses (lookup-binding (mtch-bindings m) 'names)] ...)
-                              #,body))
-                  (λ (output)
-                    (check-judgment-form-contract `#,name output compiled-output-ctcs 'O '#,mode)))))))]))
-  (with-syntax ([(clause-proc ...) (map compile-clause clauses)]
-                [(clause-proc-ids ...) (generate-temporaries clauses)])
-    (with-syntax ([(backwards-ids ...) (reverse (syntax->list #'(clause-proc-ids ...)))])
-      #'(let ([clause-proc-ids clause-proc] ...)
-          (λ (input)
-            (append (backwards-ids input) ...))))))
-
-(define (combine-judgment-rhses compiled-lhs input rhs check-output)
-  (define mtchs (match-pattern compiled-lhs input))
-  (cond
-    [mtchs
-     (define output-table (make-hash))
-     (for ([m (in-list mtchs)])
-       (define os (rhs m))
-       (when os
-         (for ([x (in-list os)])
-           (hash-set! output-table x #t))))
-     (define outputs (hash-map output-table (λ (k v) k)))
-     (for ([output (in-list outputs)])
-       (check-output output))
-     outputs]
-    [else '()]))
-
-(define-for-syntax (do-compile-judgment-form-lws clauses)
-  (syntax-case clauses ()
-    [(((_ . conc-body) . prems) ...)
-     (let ([rev-premss
-            ; for consistency with metafunction extras
-            (for/list ([prems (syntax->list #'(prems ...))])
-              (reverse (syntax->list prems)))]
-           [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 description
-    (case mode
-      [(I) "input"]
-      [(O) "output"]))
-  (when contracts
-    (let loop ([rest-modes modes] [rest-terms terms] [rest-ctcs contracts] [pos 1])
-      (unless (null? rest-modes)
-        (if (eq? mode (car rest-modes))
-            (if (match-pattern (car rest-ctcs) (car rest-terms))
-                (loop (cdr rest-modes) (cdr rest-terms) (cdr rest-ctcs) (+ 1 pos))
-                (redex-error form-name "~a ~s at position ~s does not match its contract"
-                             description (car rest-terms) pos))
-            (loop (cdr rest-modes) rest-terms rest-ctcs (+ 1 pos)))))))
-
-(define-for-syntax (mode-check mode clauses nts syn-err-name orig-stx)
-  (define ((check-template bound-anywhere) temp bound)
-    (let check ([t temp])
-      (syntax-case t (unquote)
-        [(unquote . _)
-         (raise-syntax-error syn-err-name "unquote unsupported" t)]
-        [x
-         (identifier? #'x)
-         (unless (cond [(free-id-table-ref bound-anywhere #'x #f)
-                        (free-id-table-ref bound #'x #f)]
-                       [(id-binds? nts #t #'x)
-                        (term-fn? (syntax-local-value #'x (λ () #f)))]
-                       [else #t])
-           (raise-syntax-error syn-err-name "unbound pattern variable" #'x))]
-        [(u ...)
-         (for-each check (syntax->list #'(u ...)))]
-        [_ (void)])))
-  (define ((bind kind) pat bound)
-    (define-values (ids _)
-      (extract-names nts syn-err-name #t pat kind))
-    (for/fold ([b bound]) ([x ids])
-              (free-id-table-set b x #t)))
-  (define (split-body judgment)
-    (syntax-case judgment ()
-      [(form-name . body)
-       (split-by-mode (syntax->list #'body) (judgment-form-mode (syntax-local-value #'form-name)))]))
-  (define (drop-ellipses prems)
-    (syntax-case prems ()
-      [() '()]
-      [(prem maybe-ellipsis . remaining)
-       (ellipsis? #'maybe-ellipsis)
-       (syntax-case #'prem ()
-         [(form-name . _)
-          (judgment-form-id? #'form-name)
-          (cons #'prem (drop-ellipses #'remaining))]
-         [_ (raise-syntax-error syn-err-name "ellipses must follow judgment form uses" #'maybe-ellipsis)])]
-      [(prem . remaining)
-       (cons #'prem (drop-ellipses #'remaining))]))
-  (define (fold-clause pat-pos tmpl-pos acc-init clause)
-    (syntax-case clause ()
-      [(conc . prems)
-       (let-values ([(conc-in conc-out) (split-body #'conc)])
-         (check-judgment-arity orig-stx #'conc)
-         (define acc-out
-           (for/fold ([acc (foldl pat-pos acc-init conc-in)])
-                     ([prem (drop-ellipses #'prems)])
-                     (syntax-case prem ()
-                       [(-where pat tmpl)
-                        (where-keyword? #'-where)
-                        (begin
-                          (tmpl-pos #'tmpl acc)
-                          (pat-pos #'pat acc))]
-                       [(-side-condition tmpl)
-                        (side-condition-keyword? #'-side-condition)
-                        (begin (tmpl-pos #'tmpl acc)
-                               acc)]
-                       [(form-name . _)
-                        (if (judgment-form-id? #'form-name)
-                            (let-values ([(prem-in prem-out) (split-body prem)])
-                              (check-judgment-arity orig-stx prem)
-                              (for ([pos prem-in]) (tmpl-pos pos acc))
-                              (foldl pat-pos acc prem-out))
-                            (raise-syntax-error syn-err-name "expected judgment form name" #'form-name))]
-                       [_ (raise-syntax-error syn-err-name "malformed premise" prem)])))
-         (for ([pos conc-out]) (tmpl-pos pos acc-out))
-         acc-out)]))
-  (for ([clause clauses])
-    (define do-tmpl
-      (check-template
-       (fold-clause (bind 'rhs-only) void (make-immutable-free-id-table) clause)))
-    (fold-clause (bind 'rhs-only) do-tmpl (make-immutable-free-id-table) clause)))
-
-(define-syntax (generate-lws stx)
-  (syntax-case stx ()
-    [(_ relation? seq-of-lhs seq-of-lhs-for-lw seq-of-tl-side-cond/binds seq-of-rhs side-condition-unquoted?)
-     (with-syntax
-         ([(rhs/lw ...) 
-           (syntax-case #'relation? ()
-             [#t (map (λ (x) #`(list #,@(map to-lw/proc (syntax->list x))))
-                      (syntax->list #'seq-of-rhs))]
-             [#f (map to-lw/proc (syntax->list #'seq-of-rhs))])]
-          [(((bind-id/lw . bind-pat/lw) ...) ...)
-           ;; Also for pict, extract pattern bindings
-           (map name-pattern-lws (syntax->list #'seq-of-lhs))]
-          [((where/sc/lw ...) ...)
-           ;; Also for pict, extract where bindings
-           (map (λ (hm)
-                  (map
-                   (λ (lst)
-                     (syntax-case lst (unquote side-condition where)
-                       [(form-name . _)
-                        (judgment-form-id? #'form-name)
-                        #`(make-metafunc-extra-side-cond #,(to-lw/proc lst))]
-                       [(form-name . _)
-                        (judgment-form-id? #'form-name)
-                        #`(make-metafunc-extra-side-cond #,(to-lw/proc lst))]
-                       [(where pat (unquote (f _ _)))
-                        (and (or (identifier? #'pat)
-                                 (andmap identifier? (syntax->list #'pat)))
-                             (or (free-identifier=? #'f #'variable-not-in)
-                                 (free-identifier=? #'f #'variables-not-in)))
-                        (with-syntax ([(ids ...)
-                                       (map to-lw/proc
-                                            (if (identifier? #'pat)
-                                                (list #'pat)
-                                                (syntax->list #'pat)))])
-                          #`(make-metafunc-extra-fresh
-                             (list ids ...)))]
-                       [(where pat exp)
-                        #`(make-metafunc-extra-where
-                           #,(to-lw/proc #'pat) #,(to-lw/proc #'exp))]
-                       [(side-condition x)
-                        #`(make-metafunc-extra-side-cond
-                           #,(if (syntax-e #'side-condition-unquoted?)
-                                 (to-lw/uq/proc #'x)
-                                 (to-lw/proc #'x)))]
-                       [maybe-ellipsis
-                        (ellipsis? #'maybe-ellipsis)
-                        (to-lw/proc #'maybe-ellipsis)]))
-                   (visible-extras hm)))
-                (syntax->list #'seq-of-tl-side-cond/binds))]
-          [(((where-bind-id/lw . where-bind-pat/lw) ...) ...)
-           (map (λ (clauses)
-                  (for/fold ([binds '()]) ([clause (visible-extras clauses)])
-                            (syntax-case clause (where)
-                              [(form-name . pieces)
-                               (judgment-form-id? #'form-name)
-                               (let*-values ([(mode) (judgment-form-mode (syntax-local-value #'form-name))]
-                                             [(_ outs) (split-by-mode (syntax->list #'pieces) mode)])
-                                 (for/fold ([binds binds]) ([out outs])
-                                           (append (name-pattern-lws out) binds)))]
-                              [(where lhs rhs) (append (name-pattern-lws #'lhs) binds)]
-                              [_ binds])))
-                (syntax->list #'seq-of-tl-side-cond/binds))]
-          [(((rhs-bind-id/lw . rhs-bind-pat/lw/uq) ...) ...)
-           ;; Also for pict, extract pattern bindings
-           (map (λ (x) (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/uq/proc (cdr x))))
-                            (extract-term-let-binds x)))
-                (syntax->list #'seq-of-rhs))]
-          
-          [(x-lhs-for-lw ...) #'seq-of-lhs-for-lw])
-       #'(list (list x-lhs-for-lw
-                     (list (make-metafunc-extra-where bind-id/lw bind-pat/lw) ...
-                           (make-metafunc-extra-where where-bind-id/lw where-bind-pat/lw) ...
-                           (make-metafunc-extra-where rhs-bind-id/lw rhs-bind-pat/lw/uq) ...
-                           where/sc/lw ...)
-                     rhs/lw)
-               ...))]))
-
-(define-for-syntax (visible-extras extras)
-  (for/fold ([visible empty]) ([extra (syntax->list extras)])
-            (syntax-case extra (where/hidden
-                                side-condition/hidden
-                                judgment-holds)
-              [(where/hidden pat exp) visible]
-              [(side-condition/hidden x) visible]
-              [(judgment-holds judgment)
-               (cons #'judgment visible)]
-              [_ (cons extra visible)])))
-
-(define-syntax (compile-judgment-form-proc stx)
-  (syntax-case stx ()
-    [(_ judgment-form-name lang mode clauses ctcs full-def syn-err-name)
-     (let ([nts (definition-nts #'lang #'full-def (syntax-e #'syn-err-name))])
-       (mode-check (syntax->datum #'mode) (syntax->list #'clauses) nts (syntax-e #'syn-err-name) stx)
-       (do-compile-judgment-form-proc
-        (syntax-e #'judgment-form-name) 
-        (syntax->datum #'mode) 
-        (syntax->list #'clauses) 
-        #'ctcs
-        nts
-        #'lang 
-        (syntax-e #'syn-err-name)))]))
-
-(define-syntax (compiled-judgment-form-lws stx)
-  (syntax-case stx ()
-    [(_ clauses)
-     (do-compile-judgment-form-lws (syntax->list #'clauses))]))
-
 (define (build-metafunction lang cases parent-cases wrap dom-contract-pat codom-contract-pats name relation?)
   (let* ([dom-compiled-pattern (and dom-contract-pat (compile-pattern lang dom-contract-pat #f))]
          [codom-compiled-patterns (map (λ (codom-contract-pat) (compile-pattern lang codom-contract-pat #f))
@@ -2302,8 +1634,6 @@
          (λ (exp) (and (ormap (λ (lhs) (match-pattern lhs exp)) lhss-at-lang) 
                        #t))))))
 
-(define current-traced-metafunctions (make-parameter '()))
-
 (define-syntax (metafunction-form stx)
   (syntax-case stx ()
     [(_ id)
@@ -2320,11 +1650,6 @@
             stx
             #'id)))]))
 
-(define-for-syntax (mode-keyword stx)
-  (raise-syntax-error #f "keyword invalid outside of mode specification" stx))
-(define-syntax I mode-keyword)
-(define-syntax O mode-keyword)
-
 (define-syntax (::= stx)
   (raise-syntax-error #f "cannot be used outside a language definition" stx))
 
@@ -2412,7 +1737,6 @@
                    #,(syntax/loc stx (language form-name lang-name (all-names ...) (names prods ...) ...)))))))))]))
 
 (define-struct binds (source binds))
-
   
 (define-syntax (language stx)
   (syntax-case stx ()
@@ -3008,7 +2332,7 @@
                [else #f]))))
 
 (provide (rename-out [-reduction-relation reduction-relation])
-         --> fresh with ::= I O ;; macro keywords
+         ::=
          reduction-relation->rule-names
          extend-reduction-relation
          reduction-relation?
@@ -3024,13 +2348,10 @@
          define-metafunction
          define-metafunction/extension
          define-relation
-         define-judgment-form 
-         judgment-holds
          
          (rename-out [metafunction-form metafunction])
          metafunction? metafunction-proc
          in-domain?
-         current-traced-metafunctions
          metafunc-proc-lang
          metafunc-proc-pict-info
          metafunc-proc-name
@@ -3042,10 +2363,6 @@
          metafunc-proc?
          (struct-out metafunc-case)
          
-         (struct-out metafunc-extra-side-cond)
-         (struct-out metafunc-extra-where)
-         (struct-out metafunc-extra-fresh)
-         
          (struct-out binds))
 
 (provide test-match
diff --git a/collects/redex/reduction-semantics.rkt b/collects/redex/reduction-semantics.rkt
index 78a64cb040..5b83795dec 100644
--- a/collects/redex/reduction-semantics.rkt
+++ b/collects/redex/reduction-semantics.rkt
@@ -2,6 +2,7 @@
 (require scheme/contract)
 
 (require "private/reduction-semantics.rkt"
+         "private/judgment-form.rkt"
          "private/matcher.rkt"
          "private/term.rkt"
          "private/rg.rkt"
diff --git a/collects/redex/tests/rg-test.rkt b/collects/redex/tests/rg-test.rkt
index 58dc19182d..e56ff93313 100644
--- a/collects/redex/tests/rg-test.rkt
+++ b/collects/redex/tests/rg-test.rkt
@@ -2,6 +2,7 @@
 
 (require "test-util.rkt"
          "../private/reduction-semantics.rkt"
+         "../private/judgment-form.rkt"
          "../private/matcher.rkt"
          "../private/term.rkt"
          "../private/rg.rkt"