diff --git a/collects/redex/private/generate-term.rkt b/collects/redex/private/generate-term.rkt
index cff8ddc97a..7e02fd9a77 100644
--- a/collects/redex/private/generate-term.rkt
+++ b/collects/redex/private/generate-term.rkt
@@ -322,7 +322,6 @@
      (cond
        [(metafunc #'jf/mf-id)
         (let ()
-          (define relation? (term-fn-get-info (syntax-local-value #'jf/mf-id)))
           (define (signal-error whatever)
             (when (stx-pair? whatever)
               (define cr (syntax-e (stx-car whatever)))
@@ -334,28 +333,24 @@
             (raise-syntax-error 'generate-term
                                 "expected a metafunction result and a size"
                                 stx))
-          (if relation?
-              (raise-syntax-error 'generate-term
-                                  "relations are not yet supported"
-                                  stx)
-              (let ([body-code 
-                     (λ (res size)
-                       #`(generate-mf-pat language (jf/mf-id . args) #,res #,size))])
-                (syntax-case #'rest (=)
-                  [(= res) 
-                   #`(λ (size) 
-                       #,(body-code #'res #'size))]
-                  [(= res size)
-                   (body-code #'res #'size)]
-                  [(x . y)
-                   (or (not (identifier? #'x))
-                       (not (free-identifier=? #'= #'x)))
-                   (raise-syntax-error 'generate-term
-                                       "expected to find ="
-                                       stx
-                                       #'x)]
-                  [whatever
-                   (signal-error #'whatever)]))))]
+          (let ([body-code 
+                 (λ (res size)
+                   #`(generate-mf-pat language (jf/mf-id . args) #,res #,size))])
+            (syntax-case #'rest (=)
+              [(= res) 
+               #`(λ (size) 
+                   #,(body-code #'res #'size))]
+              [(= res size)
+               (body-code #'res #'size)]
+              [(x . y)
+               (or (not (identifier? #'x))
+                   (not (free-identifier=? #'= #'x)))
+               (raise-syntax-error 'generate-term
+                                   "expected to find ="
+                                   stx
+                                   #'x)]
+              [whatever
+               (signal-error #'whatever)])))]
        [(judgment-form-id? #'jf/mf-id)
         (syntax-case #'rest ()
           [() 
diff --git a/collects/redex/private/judgment-form.rkt b/collects/redex/private/judgment-form.rkt
index b8dfb75502..40af3532af 100644
--- a/collects/redex/private/judgment-form.rkt
+++ b/collects/redex/private/judgment-form.rkt
@@ -45,10 +45,6 @@
 (define-struct metafunc-extra-where (lhs rhs))
 (define-struct metafunc-extra-fresh (vars))
 
-(define-for-syntax (judgment-form-id? stx)
-  (and (identifier? stx)
-       (judgment-form? (syntax-local-value stx (λ () #f)))))
-
 (begin-for-syntax
   ;; pre: (judgment-form-id? stx) holds
   (define (lookup-judgment-form-id stx)
@@ -179,7 +175,7 @@
                     #,(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)
+       [((form-name pats ...) . after)
         (judgment-form-id? #'form-name)
         (let*-values ([(premise) (syntax-case stx () [(p . _) #'p])]
                       [(rest-clauses under-ellipsis?)
@@ -192,7 +188,7 @@
                       [(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)])
+                       (let-values ([(in out) (split-by-mode (syntax->list #'(pats ...)) mode)])
                          (if under-ellipsis?
                              (let ([ellipsis (syntax/loc premise (... ...))])
                                (values #`(#,in #,ellipsis) #`(#,out #,ellipsis)))
@@ -336,14 +332,15 @@
   (syntax-case judgment ()
     [(form-name pat ...)
      (judgment-form-id? #'form-name)
-     (let ([expected (length (judgment-form-mode (lookup-judgment-form-id #'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)))]
+     (unless (judgment-form-relation? (lookup-judgment-form-id #'form-name))
+       (let ([expected (length (judgment-form-mode (lookup-judgment-form-id #'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)]))
 
@@ -373,7 +370,7 @@
   (not-expression-context stx)
   (syntax-case stx ()
     [(def-form-id lang . body)
-     (do-extended-judgment-form #'lang (syntax-e #'def-form-id) #'body #f stx)]))
+     (do-extended-judgment-form #'lang (syntax-e #'def-form-id) #'body #f stx #f)]))
 
 (define-syntax (define-extended-judgment-form stx)
   (not-expression-context stx)
@@ -385,9 +382,112 @@
                              "expected a judgment form"
                              stx
                              #'original-id))
-       (do-extended-judgment-form #'lang 'define-extended-judgment-form #'body #'original-id stx))]))
+       (do-extended-judgment-form #'lang 'define-extended-judgment-form #'body #'original-id stx #f))]))
 
-(define-for-syntax (do-extended-judgment-form lang syn-err-name body orig stx)
+(define-syntax (define-relation stx)
+  (syntax-case stx ()
+    [(def-form-id lang . body)
+     (let-values ([(contract-name dom-ctcs codom-contracts pats)
+                   (split-out-contract stx (syntax-e #'def-form-id) #'body #t)])
+       (with-syntax* ([((name trms ...) rest ...) (car pats)]
+                      [(mode-stx ...) #`(#:mode (name I))]
+                      [(ctc-stx ...) (if dom-ctcs 
+                                         (with-syntax ([(d-ctc ...) dom-ctcs])
+                                           #`(#:contract (name (d-ctc ...)))) 
+                                         #'())]
+                      [(clauses ...) pats]
+                      [new-body #`(mode-stx ... ctc-stx ... clauses ...)])
+                     (do-extended-judgment-form #'lang (syntax-e #'def-form-id) #'new-body #f stx #t)))]))
+
+(define-for-syntax (split-out-contract stx syn-error-name rest relation?)
+  ;; initial test determines if a contract is specified or not
+  (cond
+    [(pair? (syntax-e (car (syntax->list rest))))
+     (values #f #f (list #'any) (check-clauses stx syn-error-name (syntax->list rest) relation?))]
+    [else
+     (syntax-case rest ()
+       [(id separator more ...)
+        (identifier? #'id)
+        (cond
+          [relation?
+           (let-values ([(contract clauses) 
+                         (parse-relation-contract #'(separator more ...) syn-error-name stx)])
+             (when (null? clauses)
+               (raise-syntax-error syn-error-name 
+                                   "expected clause definitions to follow domain contract"
+                                   stx))
+             (values #'id contract (list #'any) (check-clauses stx syn-error-name clauses #t)))]
+          [else
+           (unless (eq? ': (syntax-e #'separator))
+             (raise-syntax-error syn-error-name "expected a colon to follow the meta-function's name" stx #'separator))
+           (let loop ([more (syntax->list #'(more ...))]
+                      [dom-pats '()])
+             (cond
+               [(null? more)
+                (raise-syntax-error syn-error-name "expected an ->" stx)]
+               [(eq? (syntax-e (car more)) '->)
+                (define-values (raw-clauses rev-codomains)
+                  (let loop ([prev (car more)]
+                             [more (cdr more)]
+                             [codomains '()])
+                    (cond
+                      [(null? more)
+                       (raise-syntax-error syn-error-name "expected a range contract to follow" stx prev)]
+                      [else
+                       (define after-this-one (cdr more))
+                       (cond
+                         [(null? after-this-one)
+                          (values null (cons (car more) codomains))]
+                         [else
+                          (define kwd (cadr more))
+                          (cond
+                            [(member (syntax-e kwd) '(or ∨ ∪))
+                             (loop kwd 
+                                   (cddr more)
+                                   (cons (car more) codomains))]
+                            [else
+                             (values (cdr more)
+                                     (cons (car more) codomains))])])])))
+                (let ([doms (reverse dom-pats)]
+                      [clauses (check-clauses stx syn-error-name raw-clauses relation?)])
+                  (values #'id doms (reverse rev-codomains) clauses))]
+               [else
+                (loop (cdr more) (cons (car more) dom-pats))]))])]
+       [_
+        (raise-syntax-error
+         syn-error-name
+         (format "expected the name of the ~a, followed by its contract (or no name and no contract)"
+                 (if relation? "relation" "meta-function"))
+         stx
+         rest)])]))
+
+(define-for-syntax (parse-relation-contract after-name syn-error-name orig-stx)
+  (syntax-case after-name ()
+    [(subset . rest-pieces)
+     (unless (memq (syntax-e #'subset) '(⊂ ⊆))
+       (raise-syntax-error syn-error-name
+                           "expected ⊂ or ⊆ to follow the relation's name"
+                           orig-stx #'subset))
+     (let ([more (syntax->list #'rest-pieces)])
+       (when (null? more)
+         (raise-syntax-error syn-error-name 
+                             (format "expected a sequence of patterns separated by x or × to follow ~a" 
+                                     (syntax-e #'subset))
+                             orig-stx
+                             #'subset))
+       (let loop ([more (cdr more)]
+                  [arg-pats (list (car more))])
+         (cond
+           [(and (not (null? more)) (memq (syntax-e (car more)) '(x ×)))
+            (when (null? (cdr more))
+              (raise-syntax-error syn-error-name 
+                                  (format "expected a pattern to follow ~a" (syntax-e (car more)))
+                                  orig-stx (car more)))
+            (loop (cddr more)
+                  (cons (cadr more) arg-pats))]
+           [else (values (reverse arg-pats) more)])))]))
+
+(define-for-syntax (do-extended-judgment-form lang syn-err-name body orig stx is-relation?)
   (define nts (definition-nts lang stx syn-err-name))
   (define-values (judgment-form-name dup-form-names mode position-contracts clauses rule-names)
     (parse-judgment-form-body body syn-err-name stx (identifier? orig)))
@@ -395,30 +495,30 @@
     #`(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
-                         '#,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 #,rule-names #,position-contracts #,orig #,stx #,syn-err-name))
+                         #'mk-judgment-form-proc #'#,lang #'jf-lws
+                         '#,rule-names #'judgment-runtime-gen-clauses #'mk-judgment-gen-clauses #'jf-term-proc #,is-relation?))
+        (define-values (mk-judgment-form-proc mk-judgment-gen-clauses)
+          (compile-judgment-form #,judgment-form-name #,mode #,lang #,clauses #,rule-names #,position-contracts 
+                                 #,orig #,stx #,syn-err-name judgment-runtime-gen-clauses))
         (define judgment-form-runtime-proc (mk-judgment-form-proc #,lang))
-        (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))
-        (define judgment-runtime-gen-clauses (mk-judgment-gen-clauses #,lang (λ () (judgment-runtime-gen-clauses))))))
+        (define jf-lws (compiled-judgment-form-lws #,clauses #,judgment-form-name #,stx))
+        (define judgment-runtime-gen-clauses (mk-judgment-gen-clauses #,lang (λ () (judgment-runtime-gen-clauses))))
+        (define jf-term-proc (make-jf-term-proc #,judgment-form-name #,syn-err-name #,lang #,nts #,mode))))
   (syntax-property
    (values ;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-runtime-proc judgment-form-lws judgment-runtime-gen-clauses) (values))
+            (define-syntaxes (judgment-form-runtime-proc judgment-runtime-gen-clauses jf-term-proc jf-lws) (values))
             #,definitions)
         definitions))
    'disappeared-use
    (map syntax-local-introduce dup-form-names)))
 
+(define-for-syntax (jf-is-relation? jf-id)
+  (judgment-form-relation? (lookup-judgment-form-id jf-id)))
+
 (define-for-syntax (parse-judgment-form-body body syn-err-name full-stx extension?)
   (define-syntax-class pos-mode
     #:literals (I O)
@@ -467,22 +567,22 @@
         rule:expr ...)
        (let-values ([(name/mode mode)
                      (syntax-parse #'(mode ...)
-                       [((name the-mode ...)) (values #'name (car (syntax->list #'(mode ...))))]
-                       [_ 
-                        (raise-syntax-error 
-                         #f
-                         (if (null? (syntax->list #'(mode ...)))
-                             "expected definition to include a mode specification"
-                             "expected definition to include only one mode specification")
-                         full-stx)])]
+                                   [((name the-mode ...)) (values #'name (car (syntax->list #'(mode ...))))]
+                                   [_ 
+                                    (raise-syntax-error 
+                                     #f
+                                     (if (null? (syntax->list #'(mode ...)))
+                                         "expected definition to include a mode specification"
+                                         "expected definition to include only one 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 #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))])])
          (define-values (parsed-rules rule-names) (parse-rules (syntax->list #'(rule ...)))) 
          (values name/mode mode name/ctc ctc parsed-rules rule-names))]))
   (check-clauses full-stx syn-err-name rules #t)
@@ -545,12 +645,41 @@
             the-name (list (car others))))
          (loop (cdr others))]))))
 
+(define-syntax (make-jf-term-proc stx)
+  (syntax-case stx ()
+    [(_  jdg-name syn-err-name lang nts mode)
+     (if (member 'O (syntax->datum #'mode))
+         #'(λ (_)
+             (error 'syn-err-name "judgment forms with output mode positions cannot currently be used in term"))
+         (with-syntax* ([(binding ...) (generate-temporaries (cdr (syntax->list #'mode)))]
+                        [(input) (generate-temporaries (list #'input))]
+                        [body-stx (bind-withs #'syn-err-name '() #'lang (syntax->datum #'nts) 
+                                              (if (jf-is-relation? #'jdg-name)
+                                                  (list #'(jdg-name ((unquote-splicing input))))
+                                                  (list #'(jdg-name (unquote binding) ...)))
+                                              'flatten
+                                              #`(list #t)
+                                              '()
+                                              '()
+                                              #f
+                                              #f)])
+                       (if (jf-is-relation? #'jdg-name)
+                           #`(λ (input)
+                               (not (null? body-stx)))
+                           #`(λ (input)
+                               (call-with-values 
+                                (λ () (apply values input))
+                                (λ (binding ...)
+                                  (not (null? body-stx))))))))]))
+
 (define-syntax (judgment-holds/derivation stx)
   (syntax-case stx ()
     [(_ 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)
+     (and (judgment-form-id? #'form-name)
+          (when (jf-is-relation? #'form-name)
+            (raise-syntax-error (syntax-e #'stx-name) "relations not allowed" #'form-name)))
      (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)]
@@ -676,8 +805,8 @@
                   (let (clause-proc-binding ... ...)
                     (let ([prev (orig-mk lang)])
                       (λ (recur input init-jf-derivation-id)
-                       (append (prev recur input init-jf-derivation-id)
-                               clause-proc-body-backwards ...))))))
+                        (append (prev recur input init-jf-derivation-id)
+                                clause-proc-body-backwards ...))))))
             #`(λ (lang)
                 (let (clause-proc-binding ... ...)
                   (λ (recur input init-jf-derivation-id)
@@ -699,15 +828,47 @@
      outputs]
     [else '()]))
 
-(define-for-syntax (do-compile-judgment-form-lws clauses)
+(define-for-syntax (do-compile-judgment-form-lws clauses jf-name-stx full-def)
   (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))]))
+    [(((_ . conc-body) prems ...) ...)
+     (with-syntax ([((rhss ...) (sc/ws ...)) (if (jf-is-relation? jf-name-stx)
+                                                 (with-syntax ([(((rhses ...) (where/sc ...)) ...)
+                                                                (relation-split-out-rhs #'((prems ...) ...) full-def)])
+                                                   #'(((rhses ...) ...) ((where/sc ...) ...)))
+                                                 (let ([rev-premss
+                                                        ; for consistency with metafunction extras
+                                                        (for/list ([prems (syntax->list #'((prems ...) ...))])
+                                                          (reverse (syntax->list prems)))]
+                                                       [no-rhss (map (λ (_) '()) clauses)])
+                                                   (list no-rhss rev-premss)))])
+       #`(generate-lws #t (conc-body ...) #,(lhs-lws clauses) (sc/ws ...) (rhss ...) #f))]))
+
+(define-for-syntax (relation-split-out-rhs raw-rhsss orig-stx)
+  (for/list ([rhss (in-list (syntax->list raw-rhsss))])
+    (define rhses '())
+    (define sc/wheres '())
+    (for ([rhs (in-list (syntax->list rhss))])
+      (define (found-one) 
+        (set! sc/wheres (cons rhs sc/wheres)))
+      (syntax-case rhs (side-condition side-condition/hidden where where/hidden judgment-holds)
+        [(side-condition . stuff) (found-one)]
+        [(side-condition/hidden . stuff) (found-one)]
+        [(where . stuff) (found-one)]
+        [(where/hidden . stuff) (found-one)]
+        [(judgment-holds . stuff) (found-one)]
+        [_ 
+         (cond
+           [(null? sc/wheres)
+            (set! rhses (cons rhs rhses))]
+           [else
+            (raise-syntax-error 'define-relation
+                                (format "found a '~a' clause not at the end; followed by a normal, right-hand side clause"
+                                        (syntax-e (car (syntax-e (car sc/wheres)))))
+                                (last sc/wheres)
+                                #f
+                                (list  rhs))])]))
+    (list (reverse rhses)
+          (reverse sc/wheres))))
 
 (define (check-judgment-form-contract form-name term+trees contracts mode modes)
   (define terms (if (eq? mode 'O)
@@ -731,8 +892,6 @@
   (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)
@@ -752,9 +911,11 @@
   (define (split-body judgment)
     (syntax-case judgment ()
       [(form-name . body)
-       (split-by-mode (syntax->list #'body) 
+       (if (judgment-form-relation? (lookup-judgment-form-id #'form-name))
+           (values (list) (list #'(body)))
+           (split-by-mode (syntax->list #'body) 
                       (judgment-form-mode
-                       (lookup-judgment-form-id #'form-name)))]))
+                       (lookup-judgment-form-id #'form-name))))]))
   (define (drop-ellipses prems)
     (syntax-case prems ()
       [() '()]
@@ -889,14 +1050,19 @@
        (cons #'judgment visible)]
       [_ (cons extra visible)])))
 
-(define-syntax (compile-judgment-form-proc stx)
+(define-syntax (compile-judgment-form stx)
   (syntax-case stx ()
-    [(_ judgment-form-name mode-arg lang clauses rule-names ctcs orig full-def syn-err-name)
+    [(_ judgment-form-name mode-arg lang raw-clauses rule-names ctcs orig full-def syn-err-name judgment-form-runtime-gen-clauses)
      (let ([nts (definition-nts #'lang #'full-def (syntax-e #'syn-err-name))]
-           [clauses (syntax->list #'clauses)]
-	   [rule-names (syntax->datum #'rule-names)]
-           [syn-err-name (syntax-e #'syn-err-name)])
-       (mode-check (cdr (syntax->datum #'mode-arg)) clauses nts syn-err-name stx)
+           [rule-names (syntax->datum #'rule-names)]
+           [syn-err-name (syntax-e #'syn-err-name)]
+           [clauses (rewrite-relation-prems
+                     (if (jf-is-relation? #'judgment-form-name)
+                         (fix-relation-clauses (syntax-e #'judgment-form-name) (syntax->list #'raw-clauses))
+                         (syntax->list #'raw-clauses)))]
+           [mode (cdr (syntax->datum #'mode-arg))])
+       (unless (jf-is-relation? #'judgment-form-name) 
+         (mode-check (cdr (syntax->datum #'mode-arg)) clauses nts syn-err-name stx))
        (define contracts (syntax-case #'ctcs ()
                            [#f #f]
                            [(p ...)
@@ -905,20 +1071,147 @@
                                                   (rewrite-side-conditions/check-errs nts #'syn-error-name #f pat)])
                                      #'pat))
                                  (syntax->list #'(p ...)))]))
-       (do-compile-judgment-form-proc #'judgment-form-name
-                                      #'mode-arg
-                                      clauses
-				      rule-names
-                                      contracts
-                                      nts
-                                      #'orig
-                                      #'full-def
-                                      syn-err-name))]))
+       (define proc-stx (do-compile-judgment-form-proc #'judgment-form-name
+                                                       #'mode-arg
+                                                       clauses
+                                                       rule-names
+                                                       contracts
+                                                       nts
+                                                       #'orig
+                                                       #'full-def
+                                                       syn-err-name))
+       (define gen-stx (with-syntax* ([(comp-clauses ...) 
+                                       (map (λ (c) (compile-gen-clause c mode nts syn-err-name 
+                                                                       #'judgment-form-name #'lang)) 
+                                            clauses)])
+                                     (if (identifier? #'orig)
+                                         (with-syntax ([prev-mk (judgment-form-mk-gen-clauses (lookup-judgment-form-id #'orig))])
+                                           #`(λ (effective-lang judgment-form-runtime-gen-clauses)
+                                               (define mk-prev-clauses (prev-mk effective-lang judgment-form-runtime-gen-clauses))
+                                               (λ ()
+                                                 (append 
+                                                  (mk-prev-clauses)
+                                                  #,(check-pats
+                                                     #'(list comp-clauses ...))))))
+                                         #`(λ (effective-lang judgment-form-runtime-gen-clauses)
+                                             (λ ()
+                                               #,(check-pats
+                                                  #'(list comp-clauses ...)))))))
+       #`(values #,(do-compile-judgment-form-proc #'judgment-form-name
+                                                       #'mode-arg
+                                                       clauses
+                                                       rule-names
+                                                       contracts
+                                                       nts
+                                                       #'orig
+                                                       #'full-def
+                                                       syn-err-name)
+                 #,(with-syntax* ([(comp-clauses ...) 
+                                       (map (λ (c) (compile-gen-clause c mode nts syn-err-name 
+                                                                       #'judgment-form-name #'lang)) 
+                                            clauses)])
+                                     (if (identifier? #'orig)
+                                         (with-syntax ([prev-mk (judgment-form-mk-gen-clauses (lookup-judgment-form-id #'orig))])
+                                           #`(λ (effective-lang judgment-form-runtime-gen-clauses)
+                                               (define mk-prev-clauses (prev-mk effective-lang judgment-form-runtime-gen-clauses))
+                                               (λ ()
+                                                 (append 
+                                                  (mk-prev-clauses)
+                                                  #,(check-pats
+                                                     #'(list comp-clauses ...))))))
+                                         #`(λ (effective-lang judgment-form-runtime-gen-clauses)
+                                             (λ ()
+                                               #,(check-pats
+                                                  #'(list comp-clauses ...))))))))]))
+
+(define-for-syntax (rewrite-relation-prems clauses)
+  (map (λ (c)
+         (syntax-case c ()
+           [(conc prems ...)
+            (with-syntax ([(new-prems ...) (map (λ (p)
+                                                  (syntax-case p ()
+                                                    [(r-name rest ...)
+                                                     (and (identifier? #'r-name)
+                                                          (judgment-form-id? #'r-name)
+                                                          (jf-is-relation? #'r-name))
+                                                     #'(r-name (rest ...))]
+                                                    [else
+                                                     p]))
+                                                (syntax->list #'(prems ...)))])
+              #'(conc new-prems ...))]))
+       clauses))
+
+(define-for-syntax (fix-relation-clauses name raw-clauses)
+  (map (λ (clause-stx)
+         (define (fix-rule rule-stx)
+           (syntax-case rule-stx ()
+             [(rule-name rest ...)
+              (and (identifier? #'rule-name)
+                   (judgment-form-id? #'rule-name))
+              #'(rule-name rest ...)]
+             [rule
+              #'(side-condition rule)]))
+         (let loop ([c-stx clause-stx]
+                    [new-c-stx '()]
+                    [extra-stx '()])
+           (syntax-case c-stx ()
+             [()
+              (let* ([c-rev (reverse new-c-stx)]
+                     [conclusion (syntax-case (car c-rev) ()
+                                   [(r-name rest ...)
+                                    #'(r-name (rest ...))])])
+                (with-syntax ([(cls ...) (cons conclusion (append (reverse extra-stx) (cdr c-rev)))])
+                  #'(cls ...)))]
+             [((where ext-rest ...) rest ...)
+              (where-keyword? #'where)
+              (loop #'(rest ...)
+                    new-c-stx
+                    (cons #'(where ext-rest ...) extra-stx))]
+             [((side-con ext-rest ...) rest ...)
+              (side-condition-keyword? #'side-con)
+              (loop #'(rest ...)
+                    new-c-stx
+                    (cons #'(side-con (unquote ext-rest ...)) extra-stx))]
+             [(rule ellipsis rest ...)
+              (ellipsis? #'ellipsis)
+              (loop #'(rest ...)
+                    (cons #'ellipsis (cons (fix-rule #'rule) new-c-stx))
+                    extra-stx)]
+             [(rule rest ...)
+              (loop #'(rest ...)
+                    (cons (fix-rule #'rule) new-c-stx)
+                    extra-stx)])))
+       raw-clauses))
+
+(define-syntax (compile-judgment-gen-clauses stx)
+  (syntax-case stx ()
+    [(_ judgment-form-name mode-arg lang clauses ctcs orig full-def syn-err-name judgment-form-runtime-gen-clauses)
+     (let ([clauses (syntax->list #'clauses)]
+           [nts (definition-nts #'lang #'full-def (syntax-e #'syn-err-name))]
+           [syn-err-name (syntax-e #'syn-err-name)]
+           [mode (cdr (syntax->datum #'mode-arg))])
+       (with-syntax* ([(comp-clauses ...) 
+                       (map (λ (c) (compile-gen-clause c mode nts syn-err-name 
+                                                       #'judgment-form-name #'lang)) 
+                            clauses)])
+                     (if (identifier? #'orig)
+                         (with-syntax ([prev-mk (judgment-form-mk-gen-clauses (lookup-judgment-form-id #'orig))])
+                           #`(λ (effective-lang judgment-form-runtime-gen-clauses)
+                               (define mk-prev-clauses (prev-mk effective-lang judgment-form-runtime-gen-clauses))
+                               (λ ()
+                                 (append 
+                                  (mk-prev-clauses)
+                                  #,(check-pats
+                                     #'(list comp-clauses ...))))))
+                         #`(λ (effective-lang judgment-form-runtime-gen-clauses)
+                             (λ ()
+                               #,(check-pats
+                                  #'(list comp-clauses ...)))))))]))
 
 (define-syntax (compiled-judgment-form-lws stx)
   (syntax-case stx ()
-    [(_ clauses)
-     (do-compile-judgment-form-lws (syntax->list #'clauses))]))
+    [(_ clauses name def-stx)
+     (do-compile-judgment-form-lws (syntax->list #'clauses) #'name #'def-stx)]))
 
 (define-for-syntax (extract-term-let-binds lhs)
   (let loop ([lhs lhs])
@@ -1044,32 +1337,6 @@
 ;                                                                        
 
 
-(define-syntax (compile-judgment-gen-clauses stx)
-  (syntax-case stx ()
-    [(_ judgment-form-name mode-arg lang clauses ctcs orig full-def syn-err-name judgment-form-runtime-gen-clauses)
-     (let ([clauses (syntax->list #'clauses)]
-           [nts (definition-nts #'lang #'full-def (syntax-e #'syn-err-name))]
-           [syn-err-name (syntax-e #'syn-err-name)]
-           [mode (cdr (syntax->datum #'mode-arg))])
-       (with-syntax* ([(comp-clauses ...) 
-                       (map (λ (c) (compile-gen-clause c mode nts syn-err-name 
-                                                       #'judgment-form-name #'lang)) 
-                            clauses)])
-                     (if (identifier? #'orig)
-                         (with-syntax ([prev-mk (judgment-form-mk-gen-clauses (lookup-judgment-form-id #'orig))])
-                           #`(λ (effective-lang judgment-form-runtime-gen-clauses)
-                               (define mk-prev-clauses (prev-mk effective-lang judgment-form-runtime-gen-clauses))
-                               (λ ()
-                                 (append 
-                                  (mk-prev-clauses)
-                                  #,(check-pats
-                                     #'(list comp-clauses ...))))))
-                         #`(λ (effective-lang judgment-form-runtime-gen-clauses)
-                             (λ ()
-                               #,(check-pats
-                                  #'(list comp-clauses ...)))))))]))
-
-
 
 
 (define-for-syntax (compile-gen-clause clause-stx mode nts syn-error-name jdg-name lang)
@@ -1201,6 +1468,7 @@
      #f]))
 
 (provide define-judgment-form 
+         define-relation
          define-extended-judgment-form
          judgment-holds
          build-derivations
@@ -1216,7 +1484,8 @@
                      ellipsis?
                      visible-extras
                      judgment-form-id?
-                     lookup-judgment-form-id))
+                     lookup-judgment-form-id
+                     split-out-contract))
 
 
 (provide --> fresh with I O ;; macro keywords
@@ -1236,4 +1505,5 @@
                      rewrite-prems
                      with-syntax*
                      definition-nts
-                     check-pats))
+                     check-pats
+                     relation-split-out-rhs))
diff --git a/collects/redex/private/pict.rkt b/collects/redex/private/pict.rkt
index 8ac72bb820..1e56afaa5c 100644
--- a/collects/redex/private/pict.rkt
+++ b/collects/redex/private/pict.rkt
@@ -779,13 +779,9 @@
 
 (define-syntax (render-relation stx)
   (syntax-case stx ()
-    [(form name)
-     (identifier? #'name)
-     #'(render-relation/proc 'form (metafunction name) #f)]
-    [(form name #:file filename)
-     (identifier? #'name)
-     #'(render-relation/proc 'form (metafunction name) filename)]))
-
+    [(form rest ...)
+     #'(render-judgment-form rest ...)]))
+               
 (define linebreaks (make-parameter #f))
 
 (define metafunction-pict-style (make-parameter 'left-right))
@@ -845,9 +841,6 @@
        (cons (car l) (loop (cdr l)))])))
 
 (define (metafunctions->pict/proc mfs name)
-  (for ([mf (in-list mfs)])
-    (when (metafunc-proc-relation? (metafunction-proc mf))
-      (error name "expected metafunction as argument, got a relation")))
   (unless (andmap (λ (mf) (eq? (metafunc-proc-lang (metafunction-proc (car mfs)))
                                (metafunc-proc-lang (metafunction-proc mf))))
                   mfs)
@@ -1066,19 +1059,6 @@
      (parameterize ([dc-for-text-size (make-object bitmap-dc% (make-object bitmap% 1 1))])
        (metafunctions->pict/proc mfs name))]))
 
-(define (render-relation/proc form mf filename)
-  (render-pict (λ () (inference-rules-pict/relation form mf))
-               filename))
-
-(define (inference-rules-pict/relation form mf)
-  (unless (metafunc-proc-relation? (metafunction-proc mf))
-    (error form "expected relation as argument, got a metafunction"))
-  (inference-rules-pict (metafunc-proc-name (metafunction-proc mf))
-                        (metafunc-proc-pict-info (metafunction-proc mf))
-                        (map (λ (x) #f) (metafunc-proc-pict-info (metafunction-proc mf)))
-                        (metafunc-proc-lang (metafunction-proc mf))
-                        #f))
-
 (define (render-pict make-pict filename)
   (cond
     [filename
@@ -1169,12 +1149,15 @@
 
 (define-for-syntax (inference-rules-pict/judgment-form form-name)
   (define jf (syntax-local-value form-name))
+  (define-values (name lws rule-names lang relation?) 
+    (values (judgment-form-name jf) (judgment-form-lws jf) (judgment-form-rule-names jf)
+            (judgment-form-lang jf) (judgment-form-relation? jf)))
   (syntax-property
-   #`(inference-rules-pict '#,(judgment-form-name jf)
-                           #,(judgment-form-lws jf)
-                           '#,(judgment-form-rule-names jf)
-                           #,(judgment-form-lang jf)
-                           #t)
+   #`(inference-rules-pict '#,name
+                           #,lws
+                           '#,rule-names
+                           #,lang
+                           #,(not relation?))
    'disappeared-use
    (syntax-local-introduce form-name)))
 
diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt
index edbcb74af1..88a8ff9041 100644
--- a/collects/redex/private/reduction-semantics.rkt
+++ b/collects/redex/private/reduction-semantics.rkt
@@ -1117,29 +1117,21 @@
 (define-syntax (define-metafunction stx)
   (syntax-case stx ()
     [(_ . rest)
-     (internal-define-metafunction stx #f #'rest #f)]))
-
-(define-syntax (define-relation stx)
-  (syntax-case stx ()
-    [(_ . rest)
-     ;; need to rule out the contracts for this one
-     (internal-define-metafunction stx #f #'rest #t)]))
+     (internal-define-metafunction stx #f #'rest)]))
 
 (define-syntax (define-metafunction/extension stx)
   (syntax-case stx ()
     [(_ prev . rest)
      (identifier? #'prev)
-     (internal-define-metafunction stx #'prev #'rest #f)]))
+     (internal-define-metafunction stx #'prev #'rest)]))
 
-(define-for-syntax (internal-define-metafunction orig-stx prev-metafunction stx relation?)
+(define-for-syntax (internal-define-metafunction orig-stx prev-metafunction stx)
   (not-expression-context orig-stx)
   (syntax-case stx ()
     [(lang . rest)
-     (let ([syn-error-name (if relation?
-                               'define-relation
-                               (if prev-metafunction
-                                   'define-metafunction/extension
-                                   'define-metafunction))])
+     (let ([syn-error-name (if prev-metafunction
+                               'define-metafunction/extension
+                               'define-metafunction)])
        ;; keep this near the beginning, so it signals the first error (PR 10062)
        (definition-nts #'lang orig-stx syn-error-name)
        (when (null? (syntax-e #'rest))
@@ -1150,7 +1142,7 @@
           (λ ()
             (raise-syntax-error syn-error-name "expected a previously defined metafunction" orig-stx prev-metafunction))))
        (let*-values ([(contract-name dom-ctcs codom-contracts pats)
-                      (split-out-contract orig-stx syn-error-name #'rest relation?)]
+                      (split-out-contract orig-stx syn-error-name #'rest #f)]
                      [(name _) (defined-name (list contract-name) pats orig-stx)])
          (when (and prev-metafunction (eq? (syntax-e #'name) (syntax-e prev-metafunction)))
            (raise-syntax-error syn-error-name
@@ -1169,9 +1161,8 @@
                                                             #,dom-ctcs
                                                             #,codom-contracts
                                                             #,pats
-                                                            #,relation?
                                                             #,syn-error-name))
-                                   (term-define-fn name name2 #,relation?))])
+                                   (term-define-fn name name2))])
              (if (eq? 'top-level (syntax-local-context))
                  ; Introduce the names before using them, to allow
                  ; metafunction definition at the top-level.
@@ -1181,52 +1172,19 @@
                     defs))
                  (syntax defs))))))]))
 
-(define-for-syntax (relation-split-out-rhs raw-rhsss orig-stx)
-  (for/list ([rhss (in-list (syntax->list raw-rhsss))])
-    (define rhses '())
-    (define sc/wheres '())
-    (for ([rhs (in-list (syntax->list rhss))])
-      (define (found-one) 
-        (set! sc/wheres (cons rhs sc/wheres)))
-      (syntax-case rhs (side-condition side-condition/hidden where where/hidden judgment-holds)
-        [(side-condition . stuff) (found-one)]
-        [(side-condition/hidden . stuff) (found-one)]
-        [(where . stuff) (found-one)]
-        [(where/hidden . stuff) (found-one)]
-        [(judgment-holds . stuff) (found-one)]
-        [_ 
-         (cond
-           [(null? sc/wheres)
-            (set! rhses (cons rhs rhses))]
-           [else
-            (raise-syntax-error 'define-relation
-                                (format "found a '~a' clause not at the end; followed by a normal, right-hand side clause"
-                                        (syntax-e (car (syntax-e (car sc/wheres)))))
-                                (last sc/wheres)
-                                #f
-                                (list  rhs))])]))
-    (list (reverse rhses)
-          (reverse sc/wheres))))
-
 (define-syntax (generate-metafunction stx)
   (syntax-case stx ()
-    [(_ orig-stx lang prev-metafunction name name-predicate dom-ctcs codom-contracts pats relation? syn-error-name)
+    [(_ orig-stx lang prev-metafunction name name-predicate dom-ctcs codom-contracts pats syn-error-name)
      (let ([prev-metafunction (and (syntax-e #'prev-metafunction) #'prev-metafunction)]
            [dom-ctcs (syntax-e #'dom-ctcs)]
            [codom-contracts (syntax-e #'codom-contracts)]
            [pats (syntax-e #'pats)]
-           [relation? (syntax-e #'relation?)]
            [syn-error-name (syntax-e #'syn-error-name)])
        (define lang-nts
          (definition-nts #'lang #'orig-stx syn-error-name))
        (with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats]
                      [(lhs-for-lw ...) (lhs-lws pats)])
-         (with-syntax ([((rhs stuff ...) ...) (if relation?
-                                                  (with-syntax ([(((rhses ...) (where/sc ...)) ...) 
-                                                                 (relation-split-out-rhs #'((raw-rhses ...) ...)
-                                                                                         #'orig-stx)])
-                                                    #'(((AND rhses ...) where/sc ...) ...))
-                                                  #'((raw-rhses ...) ...))]
+         (with-syntax ([((rhs stuff ...) ...) #'((raw-rhses ...) ...)]
                        [(lhs ...) #'((lhs-clauses ...) ...)])
            (parse-extras #'((stuff ...) ...))
            (with-syntax ([((side-conditions-rewritten lhs-names lhs-namess/ellipses) ...) 
@@ -1301,30 +1259,24 @@
                               (map (λ (names names/ellipses rhs/where)
                                      (with-syntax ([(names ...) names]
                                                    [(names/ellipses ...) names/ellipses]
-                                                   [rhs/where rhs/where]
-                                                   [relation? relation?])
+                                                   [rhs/where rhs/where])
                                        (syntax
                                         (λ (name bindings)
-                                          (term-let-fn ((name name relation?))
+                                          (term-let-fn ((name name))
                                                        (term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
                                                                  rhs/where))))))
                                    (syntax->list #'(lhs-names ...))
                                    (syntax->list #'(lhs-namess/ellipses ...))
                                    (syntax->list (syntax (rhs/wheres ...))))]
                              [((gen-clause lhs-pat) ...)
-                              (if relation?
-                                  (make-rl-clauses (syntax->list #'(lhs ...))
-                                                   (syntax->list #'((raw-rhses ...) ...))
-                                                   lang-nts syn-error-name #'name #'lang)
-                                  (make-mf-clauses (syntax->list #'(lhs ...))
-                                                   (syntax->list #'(rhs ...))
-                                                   (syntax->list #'((stuff ...) ...))
-                                                   lang-nts syn-error-name #'name #'lang))])
+                              (make-mf-clauses (syntax->list #'(lhs ...))
+                                               (syntax->list #'(rhs ...))
+                                               (syntax->list #'((stuff ...) ...))
+                                               lang-nts syn-error-name #'name #'lang)])
                  (syntax-property
                   (prune-syntax
                    #`(let ([sc `(side-conditions-rewritten ...)]
                            [dsc `dom-side-conditions-rewritten])
-                       ;(printf "rhs/ws: ~s\rg-rhs/ws: ~s\n" '(rhs/wheres ...) '(rg-rhs/wheres ...))
                        (let ([cases (map (λ (pat rhs-fn rg-lhs src)
                                            (make-metafunc-case
                                             (λ (effective-lang) (compile-pattern effective-lang pat #t))
@@ -1346,13 +1298,11 @@
                           (λ (f/dom)
                             (make-metafunc-proc
                              (let ([name (lambda (x) (f/dom x))]) name)
-                             (generate-lws #,relation?
+                             (generate-lws #f
                                            (lhs ...)
                                            (lhs-for-lw ...)
                                            ((stuff ...) ...)
-                                           #,(if relation?
-                                                 #'((raw-rhses ...) ...)
-                                                 #'(rhs ...))
+                                           (rhs ...)
                                            #t)
                              lang
                              #t ;; multi-args?
@@ -1360,11 +1310,7 @@
                              (let ([name (lambda (x) (name-predicate x))]) name)
                              dsc
                              (append cases parent-cases)
-                             #,relation?
                              #,(cond
-                                 [relation?
-                                  #'(λ ()
-                                      (error 'define-relation "not yet supported by generation"))]
                                  [prev-metafunction
                                   #`(extend-mf-clauses #,(term-fn-get-id (syntax-local-value prev-metafunction))
                                                        (λ ()
@@ -1380,8 +1326,7 @@
                                    #`new-lhs-pats)))
                           #,(if dom-ctcs #'dsc #f)
                           `(codom-side-conditions-rewritten ...)
-                          'name
-                          #,relation?))))
+                          'name))))
                   'disappeared-use
                   (map syntax-local-introduce 
                        (syntax->list #'(original-names ...))))))))))]))
@@ -1479,67 +1424,6 @@
             the-name (list (car others))))
          (loop (cdr others))]))))
 
-(define-for-syntax (split-out-contract stx syn-error-name rest relation?)
-  ;; initial test determines if a contract is specified or not
-  (cond
-    [(pair? (syntax-e (car (syntax->list rest))))
-     (values #f #f (list #'any) (check-clauses stx syn-error-name (syntax->list rest) relation?))]
-    [else
-     (syntax-case rest ()
-       [(id separator more ...)
-        (identifier? #'id)
-        (cond
-          [relation?
-           (let-values ([(contract clauses) 
-                         (parse-relation-contract #'(separator more ...) syn-error-name stx)])
-             (when (null? clauses)
-               (raise-syntax-error syn-error-name 
-                                   "expected clause definitions to follow domain contract"
-                                   stx))
-             (values #'id contract (list #'any) (check-clauses stx syn-error-name clauses #t)))]
-          [else
-           (unless (eq? ': (syntax-e #'separator))
-             (raise-syntax-error syn-error-name "expected a colon to follow the meta-function's name" stx #'separator))
-           (let loop ([more (syntax->list #'(more ...))]
-                      [dom-pats '()])
-             (cond
-               [(null? more)
-                (raise-syntax-error syn-error-name "expected an ->" stx)]
-               [(eq? (syntax-e (car more)) '->)
-                (define-values (raw-clauses rev-codomains)
-                  (let loop ([prev (car more)]
-                             [more (cdr more)]
-                             [codomains '()])
-                    (cond
-                      [(null? more)
-                       (raise-syntax-error syn-error-name "expected a range contract to follow" stx prev)]
-                      [else
-                       (define after-this-one (cdr more))
-                       (cond
-                         [(null? after-this-one)
-                          (values null (cons (car more) codomains))]
-                         [else
-                          (define kwd (cadr more))
-                          (cond
-                            [(member (syntax-e kwd) '(or ∨ ∪))
-                             (loop kwd 
-                                   (cddr more)
-                                   (cons (car more) codomains))]
-                            [else
-                             (values (cdr more)
-                                     (cons (car more) codomains))])])])))
-                (let ([doms (reverse dom-pats)]
-                      [clauses (check-clauses stx syn-error-name raw-clauses relation?)])
-                  (values #'id doms (reverse rev-codomains) clauses))]
-               [else
-                (loop (cdr more) (cons (car more) dom-pats))]))])]
-       [_
-        (raise-syntax-error
-         syn-error-name
-         (format "expected the name of the ~a, followed by its contract (or no name and no contract)"
-                 (if relation? "relation" "meta-function"))
-         stx
-         rest)])]))
 
 (define-for-syntax (parse-extras extras)
   (for-each
@@ -1575,33 +1459,8 @@
       (syntax->list stuffs)))
    (syntax->list extras)))
 
-(define-for-syntax (parse-relation-contract after-name syn-error-name orig-stx)
-  (syntax-case after-name ()
-    [(subset . rest-pieces)
-     (unless (memq (syntax-e #'subset) '(⊂ ⊆))
-       (raise-syntax-error syn-error-name
-                           "expected ⊂ or ⊆ to follow the relation's name"
-                           orig-stx #'subset))
-     (let ([more (syntax->list #'rest-pieces)])
-       (when (null? more)
-         (raise-syntax-error syn-error-name 
-                             (format "expected a sequence of patterns separated by x or × to follow ~a" 
-                                     (syntax-e #'subset))
-                             orig-stx
-                             #'subset))
-       (let loop ([more (cdr more)]
-                  [arg-pats (list (car more))])
-         (cond
-           [(and (not (null? more)) (memq (syntax-e (car more)) '(x ×)))
-            (when (null? (cdr more))
-              (raise-syntax-error syn-error-name 
-                                  (format "expected a pattern to follow ~a" (syntax-e (car more)))
-                                  orig-stx (car more)))
-            (loop (cddr more)
-                  (cons (cadr more) arg-pats))]
-           [else (values (reverse arg-pats) more)])))]))
 
-(define (build-metafunction lang cases parent-cases wrap dom-contract-pat codom-contract-pats name relation?)
+(define (build-metafunction lang cases parent-cases wrap dom-contract-pat codom-contract-pats name)
   (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))
                                        codom-contract-pats)]
@@ -1609,7 +1468,6 @@
          [lhss-at-lang (map (λ (case) ((metafunc-case-lhs case) lang)) all-cases)]
          [rhss-at-lang (map (λ (case) ((metafunc-case-rhs case) lang)) all-cases)]
          [ids (map metafunc-case-id all-cases)])
-    ;(printf "all-cases: ~s\nhsss: ~s\nrhsss: ~s\nids: ~s\n" all-cases lhss-at-lang rhss-at-lang ids)
     (values
      (wrap
       (letrec ([cache (make-hash)]
@@ -1648,11 +1506,7 @@
                                   [num (- (length parent-cases))])
                          (cond
                            [(null? ids) 
-                            (if relation?
-                                (begin 
-                                  (cache-result exp #f #f)
-                                  #f)
-                                (redex-error name "no clauses matched for ~s" `(,name . ,exp)))]
+                            (redex-error name "no clauses matched for ~s" `(,name . ,exp))]
                            [else
                             (let ([pattern (car lhss)]
                                   [rhs (car rhss)]
@@ -1661,22 +1515,6 @@
                               (let ([mtchs (match-pattern pattern exp)])
                                 (cond
                                   [(not mtchs) (continue)]
-                                  [relation? 
-                                   (let ([ans
-                                          (ormap (λ (mtch) 
-                                                   (define rhs-ans (rhs traced-metafunc (mtch-bindings mtch)))
-                                                   (and rhs-ans (ormap values rhs-ans)))
-                                                 mtchs)])
-                                     (unless (ormap (λ (codom-compiled-pattern) (match-pattern codom-compiled-pattern ans))
-                                                    codom-compiled-patterns)
-                                       (redex-error name "codomain test failed for ~s, call was ~s" ans `(,name ,@exp)))
-                                     (cond
-                                       [ans 
-                                        (cache-result exp #t id)
-                                        (log-coverage id)
-                                        #t]
-                                       [else
-                                        (continue)]))]
                                   [else
                                    (let ([anss (apply append
                                                       (filter values
@@ -2462,7 +2300,6 @@
          metafunc-proc-in-dom?
          metafunc-proc-dom-pat
          metafunc-proc-cases
-         metafunc-proc-relation?
          metafunc-proc?
          (struct-out metafunc-case)
          
@@ -2502,12 +2339,3 @@
          coverage?)
 
 (provide do-test-match)
-
-;; the AND metafunction is defined here to be used
-;; in define-relation so that ellipses work properly
-;; across clauses in relations
-(define-language and-L)
-(define-metafunction and-L
-  AND : any ... -> any
-  [(AND any ...) 
-   ,(andmap values (term (any ...)))])
diff --git a/collects/redex/private/term-fn.rkt b/collects/redex/private/term-fn.rkt
index 78b7e2a7c0..839d76b73c 100644
--- a/collects/redex/private/term-fn.rkt
+++ b/collects/redex/private/term-fn.rkt
@@ -4,7 +4,6 @@
 (provide make-term-fn
          term-fn?
          term-fn-get-id
-         term-fn-get-info
          (struct-out term-id)
          
          (struct-out judgment-form)
@@ -21,7 +20,6 @@
          metafunc-proc-in-dom?
          metafunc-proc-dom-pat
          metafunc-proc-cases
-         metafunc-proc-relation?
          metafunc-proc-gen-clauses
          metafunc-proc-lhs-pats
          metafunc-proc?
@@ -32,9 +30,8 @@
          pattern-symbols)
 
 (define-values (struct-type make-term-fn term-fn? term-fn-get term-fn-set!) 
-  (make-struct-type 'term-fn #f 2 0))
+  (make-struct-type 'term-fn #f 1 0))
 (define term-fn-get-id (make-struct-field-accessor term-fn-get 0))
-(define term-fn-get-info (make-struct-field-accessor term-fn-get 1))
 
 (define-struct term-id (id depth))
 
@@ -43,7 +40,7 @@
        (cond [(syntax-local-value stx (λ () #f)) => p?]
              [else #f])))
 
-(define-struct judgment-form (name mode proc mk-proc lang lws rule-names gen-clauses mk-gen-clauses)
+(define-struct judgment-form (name mode proc mk-proc lang lws rule-names gen-clauses mk-gen-clauses term-proc relation?)
   #:transparent)
 
 (define-struct defined-term (value))
@@ -75,7 +72,7 @@
                               variable-not-otherwise-mentioned hole symbol))
 
 (define-values (struct:metafunc-proc make-metafunc-proc metafunc-proc? metafunc-proc-ref metafunc-proc-set!)
-  (make-struct-type 'metafunc-proc #f 11 0 #f null (current-inspector) 0))
+  (make-struct-type 'metafunc-proc #f 10 0 #f null (current-inspector) 0))
 (define metafunc-proc-pict-info (make-struct-field-accessor metafunc-proc-ref 1))
 (define metafunc-proc-lang (make-struct-field-accessor metafunc-proc-ref 2))
 (define metafunc-proc-multi-arg? (make-struct-field-accessor metafunc-proc-ref 3))
@@ -83,6 +80,5 @@
 (define metafunc-proc-in-dom? (make-struct-field-accessor metafunc-proc-ref 5))
 (define metafunc-proc-dom-pat (make-struct-field-accessor metafunc-proc-ref 6))
 (define metafunc-proc-cases (make-struct-field-accessor metafunc-proc-ref 7))
-(define metafunc-proc-relation? (make-struct-field-accessor metafunc-proc-ref 8))
-(define metafunc-proc-gen-clauses (make-struct-field-accessor metafunc-proc-ref 9))
-(define metafunc-proc-lhs-pats (make-struct-field-accessor metafunc-proc-ref 10))
+(define metafunc-proc-gen-clauses (make-struct-field-accessor metafunc-proc-ref 8))
+(define metafunc-proc-lhs-pats (make-struct-field-accessor metafunc-proc-ref 9))
diff --git a/collects/redex/private/term.rkt b/collects/redex/private/term.rkt
index 2120b6962f..6cc5dbb85f 100644
--- a/collects/redex/private/term.rkt
+++ b/collects/redex/private/term.rkt
@@ -18,7 +18,8 @@
          term/nts
          (for-syntax term-rewrite
                      term-temp->pat
-                     currently-expanding-term-fn))
+                     currently-expanding-term-fn
+                     judgment-form-id?))
 
 (define-syntax (hole stx) (raise-syntax-error 'hole "used outside of term"))
 (define-syntax (in-hole stx) (raise-syntax-error 'in-hole "used outside of term"))
@@ -31,6 +32,10 @@
 (define-for-syntax lang-keyword
   (list '#:lang #f))
 
+(define-for-syntax (judgment-form-id? stx)
+  (and (identifier? stx)
+       (judgment-form? (syntax-local-value stx (λ () #f)))))
+
 (define-syntax (term stx)
   (syntax-case stx ()
     [(term t . kw-args)
@@ -70,6 +75,12 @@
     [(_ inner-apps)
      #'(λ (l) (map inner-apps l))]))
 
+(define-syntax (jf-apply stx)
+  (syntax-case stx ()
+    [(_ jf)
+     (judgment-form-id? #'jf)
+     (judgment-form-term-proc (syntax-local-value #'jf (λ () #f)))]))
+
 (define-for-syntax currently-expanding-term-fn (make-parameter #f))
 
 
@@ -80,7 +91,7 @@
 ;; term-binding  := `(,t-bind-pat (,mf-apps ,term-datum))
 ;; t-bind-pat    := id | (ref id) | `(,t-b-seq ...)
 ;; t-b-seq       := t-bind-pat | ellipsis
-;; mf-apps       := `(mf-map ,mf-apps) | `(mf-app ,metafunction-id)
+;; mf-apps       := `(mf-map ,mf-apps) | `(mf-apply ,metafunction-id) | `(jf-apply ,judgment-form-id)
 ;; term-datum    := `(quasidatum ,d)
 ;; d             := literal | pattern-variable | `(,d-seq ...) | ;; other (holes, undatum)
 ;; d-seq         := d | ellipsis
@@ -105,7 +116,9 @@
     (let-values ([(rewritten max-depth) (rewrite/max-depth args depth)])
       (let ([result-id (car (generate-temporaries '(f-results)))])
         (with-syntax ([fn fn])
-          (let loop ([func (syntax (mf-apply fn))]
+          (let loop ([func (if (judgment-form-id? #'fn)
+                               (syntax (jf-apply fn))
+                               (syntax (mf-apply fn)))]
                      [args-stx rewritten]
                      [res result-id]
                      [args-depth (min depth max-depth)])
@@ -134,6 +147,16 @@
        (let ([f (term-fn-get-id (syntax-local-value/record (syntax metafunc-name) (λ (x) #t)))])
          (free-identifier-mapping-put! applied-metafunctions f #t)
          (rewrite-application f (syntax/loc stx (arg ...)) depth))]
+      [(jf-name arg ...)
+       (and (identifier? (syntax jf-name))
+            (if names
+                (not (memq (syntax->datum #'jf-name) names))
+                #t)
+            (judgment-form-id? #'jf-name))
+       (begin
+         (unless (not (memq 'O (judgment-form-mode (syntax-local-value #'jf-name))))
+           (raise-syntax-error 'term "judgment forms with output mode (\"O\") positions disallowed" arg-stx stx))
+         (rewrite-application #'jf-name (syntax/loc stx (arg ...)) depth))]
       [f
        (and (identifier? (syntax f))
             (if names
@@ -291,7 +314,7 @@
 
 (define-for-syntax (bind-mf-sig->pat bmfs)
   (syntax-case bmfs ()
-    ;; TODO : handle apps at ellipsis depth 
+    ;; TODO : handle apps at ellipsis depth , handle judgment forms (I only)
     [(mf-apply f)
      (and (identifier? #'mf-apply)
           (eq? (syntax-e #'mf-apply) 'mf-apply))
@@ -299,39 +322,23 @@
 
 (define-syntax (term-let-fn stx)
   (syntax-case stx ()
-    [(_ ([f . rhs-stuff] ...) body1 body2 ...)
-     (with-syntax ([(g ...) (generate-temporaries (syntax (f ...)))]
-                   [((rhs info) ...)
-                    (for/list ([rhs-stuff (in-list (syntax->list #'(rhs-stuff ...)))]
-                               [f (in-list (syntax->list #'(f ...)))])
-                      (syntax-case rhs-stuff ()
-                        [(rhs) #'(rhs #f)]
-                        [(rhs info) #'(rhs info)]
-                        [else (raise-syntax-error 'term-let-fn 
-                                                  (format "expected the rhs of a binding for ~a"
-                                                          (syntax->datum f))
-                                                  stx f)]))])
+    [(_ ([f rhs] ...) body1 body2 ...)
+     (with-syntax ([(g ...) (generate-temporaries (syntax (f ...)))])
        (syntax 
         (let ([g rhs] ...)
-          (let-syntax ([f (make-term-fn #'g info)] ...)
+          (let-syntax ([f (make-term-fn #'g)] ...)
             body1
             body2 ...))))]))
 
 (define-syntax (term-define-fn stx)
   (syntax-case stx ()
-    [(_ id exp info)
-     ;; this info is currently used to record the 
-     ;; difference between define-metafunctions 
-     ;; bound identifiers and define-relation bound
-     ;; ones for use in the unification-based generator
+    [(_ id exp)
      (with-syntax ([id2 (datum->syntax #'here (syntax-e #'id))])
        (syntax
         (begin
           (define id2 exp)
           (define-syntax id
-            (make-term-fn #'id2 info)))))]
-    [(_ id exp)
-     #'(term-define-fn id exp #f)]))
+            (make-term-fn #'id2)))))]))
 
 (define-syntax (term-let/error-name stx)
   (syntax-case stx ()
diff --git a/collects/redex/scribblings/ref.scrbl b/collects/redex/scribblings/ref.scrbl
index cb1f4fb172..3480e7385f 100644
--- a/collects/redex/scribblings/ref.scrbl
+++ b/collects/redex/scribblings/ref.scrbl
@@ -43,11 +43,6 @@
     [(_ args ...)
      #'((tech (racketvarfont "term")) args ...)]
     [x (identifier? #'x) #'(tech (racketvarfont "term"))]))
-@(define-syntax (tttterm-no-unquote stx)
-   (syntax-case stx ()
-    [(_ args ...)
-     #'((tech (racketvarfont "term-without-unquote") #:key "term") args ...)]
-    [x (identifier? #'x) #'(tech (racketvarfont "term-without-unquote") #:key "term")]))
 
 @(define-syntax (tterm stx)
    (syntax-case stx ()
@@ -1191,10 +1186,10 @@ and @racket[#f] otherwise.
                      rule-name]]
               [conclusion (form-id pat/term ...)]
               [premise (code:line (judgment-form-id pat/term ...) maybe-ellipsis)
-                       (where @#,ttpattern @#,tttterm-no-unquote)
-                       (where/hidden @#,ttpattern @#,tttterm-no-unquote)
-                       (side-condition @#,tttterm-no-unquote)
-                       (side-condition/hidden @#,tttterm-no-unquote)]
+                       (where @#,ttpattern @#,tttterm)
+                       (where/hidden @#,ttpattern @#,tttterm)
+                       (side-condition @#,tttterm)
+                       (side-condition/hidden @#,tttterm)]
               [rule-name (code:line)
                          string
                          non-ellipsis-non-hypens-var]
@@ -1211,9 +1206,8 @@ Each rule must be such that its premises can be evaluated left-to-right
 without ``guessing'' values for any of their pattern variables. Redex checks this
 property using the mandatory @racket[mode-spec] declaration, which partitions positions
 into inputs @racket[I] and outputs @racket[O]. Output positions in conclusions
-and input positions in premises must be @|tttterm|s with no uses of 
-@racket[unquote]; input positions in conclusions and output positions in 
-premises must be @|ttpattern|s. When the optional @racket[contract-spec] 
+and input positions in premises must be @|tttterm|s; input positions in conclusions and 
+output positions in premises must be @|ttpattern|s. When the optional @racket[contract-spec] 
 declaration is present, Redex dynamically checks that the terms flowing through
 these positions match the provided patterns, raising an exception recognized by 
 @racket[exn:fail:redex] if not.
@@ -1265,8 +1259,7 @@ to compute all pairs with a given sum.
        (judgment-holds (sumr n_1 n_2 (s (s z))) (n_1 n_2))]
 
 A rule's @racket[where] and @racket[where/hidden] premises behave as in 
-@racket[reduction-relation] and @racket[define-metafunction] except the term
-cannot use unquotes.
+@racket[reduction-relation] and @racket[define-metafunction].
 @examples[
 #:eval redex-eval
        (define-judgment-form nats
@@ -1296,9 +1289,14 @@ A rule's @racket[side-condition] and @racket[side-condition/hidden] premises are
 to those in @racket[reduction-relation] and @racket[define-metafunction], except that
 they do not implicitly unquote their right-hand sides. In other words, a premise 
 of the form @racket[(side-condition term)] is equivalent to the premise 
-@racket[(where #t term)], except it does not typeset with the ``#t = '', as that would. 
-Also, the term on the right-hand side cannot use unquotes so it is often convenient to 
-define a metafunction for these side-conditions.
+@racket[(where #t term)], except it does not typeset with the ``#t = '', as that would.
+
+Judgments with exclusively @racket[I] mode positions may also be used in @|tttterm|s
+in a manner similar to metafunctions, and evaluate to a boolean.
+@examples[
+#:eval redex-eval
+       (term (le (s z) (s (s z))))
+       (term (le (s z) z))]
 
 A literal ellipsis may follow a judgment premise when a template in one of the
 judgment's input positions contains a pattern variable bound at ellipsis-depth
@@ -1452,12 +1450,6 @@ the argument contracts.
        (term (subtype int num))
        (term (subtype (int → int) (num → num)))
        (term (subtype (num → int) (num → num)))]
-
-Note that relations are assumed to always return the same results for
-the same inputs, and their results are cached, unless
-@racket[caching-enable?] is set to @racket[#f]. Accordingly, if a
-relation is called with the same inputs twice, then its right-hand
-sides are evaluated only once.
 }
 
 @defparam[current-traced-metafunctions traced-metafunctions (or/c 'all (listof symbol?))]{
diff --git a/collects/redex/tests/gen-test.rkt b/collects/redex/tests/gen-test.rkt
index a3a12c94a0..aa307e303e 100644
--- a/collects/redex/tests/gen-test.rkt
+++ b/collects/redex/tests/gen-test.rkt
@@ -63,10 +63,10 @@
               #t)
   
   (test-equal (generate-term nats #:satisfying (sum z (s z) n) +inf.0)
-              (term (sum z (s z) (s z))))
+              '(sum z (s z) (s z)))
   
   (test-equal (generate-term nats #:satisfying (sum (s z) (s z) n) +inf.0)
-              (term (sum (s z) (s z) (s (s z)))))
+              '(sum (s z) (s z) (s (s z))))
   
   (for ([_ 100])
     (match (generate-term nats #:satisfying (sum n_1 n_2 n_3) 5)
diff --git a/collects/redex/tests/run-tests.rkt b/collects/redex/tests/run-tests.rkt
index 8c7bca7515..33e1d3ccbd 100644
--- a/collects/redex/tests/run-tests.rkt
+++ b/collects/redex/tests/run-tests.rkt
@@ -24,6 +24,7 @@
      "tl-test.rkt"
      "term-test.rkt"
      "rg-test.rkt"
+     "gen-test.rkt"
      "keyword-macros-test.rkt"
      "core-layout-test.rkt"
      "pict-test.rkt"
diff --git a/collects/redex/tests/syn-err-tests/judgment-form-definition.rktd b/collects/redex/tests/syn-err-tests/judgment-form-definition.rktd
index 645179d84c..7141644f6e 100644
--- a/collects/redex/tests/syn-err-tests/judgment-form-definition.rktd
+++ b/collects/redex/tests/syn-err-tests/judgment-form-definition.rktd
@@ -142,21 +142,7 @@
      [(name)
       bad-prem])
    (void)))
-(#rx"unquote unsupported"
- ([unq ,(+ 1)])
- (let ()
-   (define-judgment-form syn-err-lang
-     #:mode (uses-unquote I)
-     [(uses-unquote n)
-      (where n unq)])
-   (void)))
-(#rx"unquote unsupported"
- ([unq ,'z])
- (let ()
-   (define-judgment-form syn-err-lang
-     #:mode (uses-unquote I O)
-     [(uses-unquote n unq)])
-   (void)))
+
 
 (#rx"missing ellipsis"
  ([use any_0]) ([ellipsis ...] [def any_0])
diff --git a/collects/redex/tests/syn-err-tests/relation-definition.rktd b/collects/redex/tests/syn-err-tests/relation-definition.rktd
index 3ff90b76ec..891d848b7f 100644
--- a/collects/redex/tests/syn-err-tests/relation-definition.rktd
+++ b/collects/redex/tests/syn-err-tests/relation-definition.rktd
@@ -20,7 +20,7 @@
  (define-relation syn-err-lang
    [(R () ())]
    [(R (any_a) (any_b)) 
-    (R anc_c any_d) 
+    (R any_c any_d) 
     first-where
     (where any_d any_b)
     first-post-where]))
diff --git a/collects/redex/tests/tl-test.rkt b/collects/redex/tests/tl-test.rkt
index cbf2c0f620..be4dc67a8a 100644
--- a/collects/redex/tests/tl-test.rkt
+++ b/collects/redex/tests/tl-test.rkt
@@ -1236,6 +1236,24 @@
     
     (test (term (R (xx) (xx))) #t)
     (test (term (R (()) ())) #f))
+  
+  (let ()
+    
+    (define-relation empty-language
+      [(a number_1)
+       (b number_1)]
+      [(a 2)])
+    
+    (define-relation empty-language
+      [(b 1)]
+      [(b 2)])
+    
+    (test (term (a 1)) #t)
+    (test (term (a 2)) #t)
+    (test (term (a 3)) #f)
+    (test (term (b 1)) #t)
+    (test (term (b 2)) #t)
+    (test (term (b 3)) #f))
 
   
   (exec-syntax-error-tests "syn-err-tests/relation-definition.rktd")
@@ -2299,7 +2317,9 @@
         [(different any_a any_a) #f]
         [(different any_a any_b) #t])
       (test (judgment-holds (R 1 2)) #t)
-      (test (judgment-holds (R 1 1)) #f))
+      (test (judgment-holds (R 1 1)) #f)
+      (test (term (R 1 2)) #t)
+      (test (term (R 1 1)) #f))
     
     (let ()
       (define-judgment-form empty-language
@@ -2441,6 +2461,79 @@
                        '(J () z)
 		       #f
                        '()))))))))
+    (let ()
+      (define-language U
+        (n Z (S n)))
+      
+      (define-judgment-form U
+        #:mode (jsum I I I)
+        [(jsum n Z n)]
+        [(jsum n_1 (S n_2) (S n_3))
+         (jsum n_1 n_2 n_3)])
+      
+      (define-relation U
+        sum ⊆ n x n x n
+        [(sum n Z n)]
+        [(sum n_1 (S n_2) (S n_3))
+         (sum n_1 n_2 n_3)])
+      
+      (define-relation U
+        [(rjsum n_1 n_2 n_3)
+         (jjsum n_1 n_2 n_3)])
+      
+      (define-judgment-form U
+        #:mode (jjsum I I I)
+        [(jjsum n_1 n_2 n_3)
+         (rrsum n_1 n_2 n_3)])
+      
+      (define-relation U
+        [(rrsum n_1 n_2 n_3)
+         (jsum n_1 n_2 n_3)])
+      
+      (test (term (sum Z Z Z)) #t)
+      (test (term (sum Z Z (S Z))) #f)
+      (test (term (sum (S Z) (S Z) (S (S Z)))) #t)
+      (test (term (sum (S Z) (S (S Z)) (S (S Z)))) #f)
+      (test (term (sum (S (S Z)) (S (S Z)) (S (S (S (S Z)))))) #t)
+      (test (term (sum (S (S Z)) (S (S Z)) (S (S (S Z))))) #f)
+      (test (term (jsum Z Z Z)) #t)
+      (test (term (jsum Z Z (S Z))) #f)
+      (test (term (jsum (S Z) (S Z) (S (S Z)))) #t)
+      (test (term (jsum (S Z) (S (S Z)) (S (S Z)))) #f)
+      (test (term (jsum (S (S Z)) (S (S Z)) (S (S (S (S Z)))))) #t)
+      (test (term (jsum (S (S Z)) (S (S Z)) (S (S (S Z))))) #f)
+      (test (term (rjsum Z Z Z)) #t)
+      (test (term (rjsum Z Z (S Z))) #f)
+      (test (term (rjsum (S Z) (S Z) (S (S Z)))) #t)
+      (test (term (rjsum (S Z) (S (S Z)) (S (S Z)))) #f)
+      (test (term (rjsum (S (S Z)) (S (S Z)) (S (S (S (S Z)))))) #t)
+      (test (term (rjsum (S (S Z)) (S (S Z)) (S (S (S Z))))) #f))
+    
+    (let ()
+      (define-judgment-form empty-language
+        #:mode (Q I O)
+        [(Q number_1 ,(+ (term number_1) (term number_1)))]
+        [(Q (number_1 number_2) number_3)
+         (Q ,(+ (term number_1) (term number_2)) number_3)])
+      
+      (test (judgment-holds (Q 1 2))
+                  #t)
+      (test (judgment-holds (Q 1 3))
+                  #f)
+      (test (judgment-holds (Q 1 number_1) number_1)
+                  '(2))
+      (test (judgment-holds (Q 7 14))
+                  #t)
+      (test (judgment-holds (Q 7 symbol))
+                  #f)
+      (test (judgment-holds (Q 7 number_1) number_1)
+                  '(14))
+      (test (judgment-holds (Q (1 2) 6))
+                  #t)
+      (test (judgment-holds (Q (1 3) 6))
+                  #f)
+      (test (judgment-holds (Q (3 4) number_1) number_1)
+                  '(14)))
 
     
     (parameterize ([current-namespace (make-base-namespace)])
@@ -2921,7 +3014,7 @@
       (parameterize ([relation-coverage (list c)])
         (term (f 1))
         (test (sorted-counts c) '(1 0 0))))
-    
+    #;
     (let ([c (make-coverage R)])
       (parameterize ([relation-coverage (list c)])
         (term (R 2))
diff --git a/doc/release-notes/redex/HISTORY.txt b/doc/release-notes/redex/HISTORY.txt
index f90b11e916..0185ba9db1 100644
--- a/doc/release-notes/redex/HISTORY.txt
+++ b/doc/release-notes/redex/HISTORY.txt
@@ -4,6 +4,11 @@ v5.3.2
     (which allows Redex to more effectively generate things
      like well-typed terms)
 
+  * removed the restriction on unquotes in define-judgment-form
+
+  * added the option to use judgment-forms with only I mode
+    positions in terms
+
 v5.3.1
 
   * added optional #:lang keyword to term