diff --git a/collects/redex/private/reduction-semantics.ss b/collects/redex/private/reduction-semantics.ss
index 8e0001be61..da20055d94 100644
--- a/collects/redex/private/reduction-semantics.ss
+++ b/collects/redex/private/reduction-semantics.ss
@@ -26,15 +26,19 @@
    (identifier-prune-lexical-context #'whatever '(#%app #%datum))
    (let loop ([stx stx])
      (syntax-case stx (quote)
-       [(quote x) (list (quote-syntax/prune quote)
-                        (syntax->datum #'x))]
-       [(a . b) (cons (loop #'a) (loop #'b))]
+       [(quote x)
+        (list (quote-syntax/prune quote)
+              (syntax->datum #'x))]
+       [(a . b)
+        (datum->syntax (identifier-prune-lexical-context #'whatever '(#%app))
+                       (cons (loop #'a) (loop #'b))
+                       stx)]
        [x 
         (identifier? #'x)
-        (datum->syntax (identifier-prune-lexical-context #'x)
-                       (syntax-e #'x))]
-       [() '()]
-       [_ (syntax->datum stx)]))))
+        (identifier-prune-lexical-context #'x)]
+       [() (datum->syntax #f '() stx)]
+       [_ (datum->syntax (identifier-prune-lexical-context #'whatever '(#%datum))
+                         (syntax->datum stx) stx)]))))
 
 (define-syntax (term-match/single stx)
   (syntax-case stx ()
@@ -1005,21 +1009,26 @@
   (define (internal-define-metafunction orig-stx prev-metafunction stx relation?)
     (syntax-case stx ()
       [(lang . rest)
-       (let ([syn-error-name (if prev-metafunction
-                                 'define-metafunction/extension
-                                 'define-metafunction)])
+       (let ([syn-error-name (if relation?
+                                 'define-relation
+                                 (if prev-metafunction
+                                     'define-metafunction/extension
+                                     'define-metafunction))])
          (unless (identifier? #'lang)
            (raise-syntax-error syn-error-name "expected an identifier in the language position" orig-stx #'lang))
          (when (null? (syntax-e #'rest))
            (raise-syntax-error syn-error-name "no clauses" orig-stx))
          (prune-syntax
           (let-values ([(contract-name dom-ctcs codom-contract pats)
-                        (split-out-contract orig-stx syn-error-name #'rest)])
-            (with-syntax ([(((original-names lhs-clauses ...) rhs stuff ...) ...) pats]
+                        (split-out-contract orig-stx syn-error-name #'rest relation?)])
+            (with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats]
                           [(lhs-for-lw ...)
-                           (with-syntax ([((lhs-for-lw _ _ ...) ...) pats])
+                           (with-syntax ([((lhs-for-lw _ ...) ...) pats])
                              (map (λ (x) (to-lw/proc (datum->syntax #f (cdr (syntax-e x)) x)))
                                   (syntax->list #'(lhs-for-lw ...))))])
+              (with-syntax ([((rhs stuff ...) ...) (if relation?
+                                                       #'((,(and (term raw-rhses) ...)) ...)
+                                                       #'((raw-rhses ...) ...))])
               (parameterize ([is-term-fn? 
                               (let ([names (syntax->list #'(original-names ...))])
                                 (λ (x) (and (not (null? names))
@@ -1057,7 +1066,7 @@
                         (with-syntax ([(side-conditions-rewritten ...) 
                                        (map (λ (x) (rewrite-side-conditions/check-errs
                                                     lang-nts
-                                                    'define-metafunction
+                                                    syn-error-name
                                                     #t
                                                     x))
                                             (syntax->list (syntax ((side-condition lhs tl-withs) ...))))]
@@ -1065,18 +1074,19 @@
                                        (and dom-ctcs
                                             (rewrite-side-conditions/check-errs
                                              lang-nts
-                                             'define-metafunction
+                                             syn-error-name
                                              #f
                                              dom-ctcs))]
                                       [codom-side-conditions-rewritten
                                        (rewrite-side-conditions/check-errs
                                         lang-nts
-                                        'define-metafunction
+                                        syn-error-name
                                         #f
                                         codom-contract)]
                                       [(rhs-fns ...)
                                        (map (λ (lhs rhs bindings)
-                                              (let-values ([(names names/ellipses) (extract-names lang-nts 'define-metafunction #t lhs)])
+                                              (let-values ([(names names/ellipses) 
+                                                            (extract-names lang-nts syn-error-name #t lhs)])
                                                 (with-syntax ([(names ...) names]
                                                               [(names/ellipses ...) names/ellipses]
                                                               [rhs rhs]
@@ -1150,7 +1160,7 @@
                                     #,relation?)))
                                (term-define-fn name name2))
                            'disappeared-use
-                           (map syntax-local-introduce (syntax->list #'(original-names ...))))))))))))))]
+                           (map syntax-local-introduce (syntax->list #'(original-names ...)))))))))))))))]
       [(_ prev-metafunction name lang clauses ...)
        (begin
          (unless (identifier? #'name)
@@ -1166,11 +1176,11 @@
           (syntax->list (syntax (clauses ...))))
          (raise-syntax-error 'define-metafunction "missing error check for bad syntax" stx))]))
 
-  (define (split-out-contract stx syn-error-name rest)
+  (define (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 #'any (check-clauses stx syn-error-name rest))]
+       (values #f #f #'any (check-clauses stx syn-error-name rest relation?))]
       [else
        (syntax-case rest ()
          [(id colon more ...)
@@ -1187,7 +1197,7 @@
                    (raise-syntax-error syn-error-name "expected a range contract to follow the arrow" stx (car more)))
                  (let ([doms (reverse dom-pats)]
                        [codomain (cadr more)]
-                       [clauses (check-clauses stx syn-error-name (cddr more))])
+                       [clauses (check-clauses stx syn-error-name (cddr more) relation?)])
                    (values #'id doms codomain clauses))]
                 [else
                  (loop (cdr more) (cons (car more) dom-pats))])))]
@@ -1198,19 +1208,21 @@
            stx
            rest)])]))
            
-  (define (check-clauses stx syn-error-name rest)
+  (define (check-clauses stx syn-error-name rest relation?)
     (syntax-case rest ()
       [([(lhs ...) roc1 roc2 ...] ...)
        rest]
       [([(lhs ...) rhs ...] ...)
-       (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)]))
-          (syntax->list #'([(lhs ...) rhs ...] ...)))
-         (raise-syntax-error syn-error-name "error checking failed.3" stx))]
+       (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)]))
+              (syntax->list #'([(lhs ...) rhs ...] ...)))
+             (raise-syntax-error syn-error-name "error checking failed.3" stx)))]
       [([x roc ...] ...)
        (begin
          (for-each 
diff --git a/collects/redex/private/tl-test.ss b/collects/redex/private/tl-test.ss
index 9f0748378e..e1ee54b582 100644
--- a/collects/redex/private/tl-test.ss
+++ b/collects/redex/private/tl-test.ss
@@ -656,6 +656,23 @@
     (test (term (<: 1 2 1 3 4)) #t)
     (test (term (<: 1 2 3 1 4)) #t)
     (test (term (<: 1 2 3 4 1)) #t))
+  
+  (let ()
+    (define-relation empty-language
+      [(<: number_1 number_1)])
+    (test (term (<: 1 1)) #t)
+    (test (term (<: 1 2)) #f))
+  
+  (let ()
+    (define-relation empty-language
+      [(<: number_1 number_2 number_3)
+       ,(= (term number_1) (term number_2))
+       ,(= (term number_2) (term number_3))])
+    (test (term (<: 1 2 3)) #f)
+    (test (term (<: 1 1 2)) #f)
+    (test (term (<: 1 2 2)) #f)
+    (test (term (<: 1 1 1)) #t))
+  
  
 ;                    ;;                         ;                                        ;;                    ;                 
 ;                     ;                 ;                                                 ;            ;                         
diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl
index ed2eed7fbf..9461f91294 100644
--- a/collects/redex/redex.scrbl
+++ b/collects/redex/redex.scrbl
@@ -982,11 +982,8 @@ and @scheme[#f] otherwise.
 
 @defform/subs[#:literals ()
               (define-relation language-exp
-               [(name @#,ttpattern ...) @#,tttterm extras ...] 
-               ...)
-               ([extras (side-condition scheme-expression)
-                        (where tl-pat @#,tttterm)]
-                [tl-pat identifier (tl-pat-ele ...)]
+               [(name @#,ttpattern ...) @#,tttterm ...] ...)
+               ([tl-pat identifier (tl-pat-ele ...)]
                 [tl-pat-ele tl-pat (code:line tl-pat ... (code:comment "a literal ellipsis"))])]{
 
 The @scheme[define-relation] form builds a relation on
@@ -995,21 +992,22 @@ expressions. The first argument indicates the language used
 to resolve non-terminals in the pattern expressions. Each of
 the rhs-expressions is implicitly wrapped in @|tttterm|. 
 
-If specified, the side-conditions are collected with 
-@scheme[and] and used as guards on the case being matched. The
-argument to each side-condition should be a Scheme
-expression, and the pattern variables in the @|ttpattern| are
-bound in that expression.
+Relations are like metafunctions in that they are called with
+arguments and return results (unlike in, say, prolog, where a relation
+definition would be able to synthesize some of the arguments based on
+the values of others).
 
 Unlike metafunctions, relations check all possible ways to match each
 case, looking for a true result and if none of the clauses match, then
-the result is @scheme[#f].
+the result is @scheme[#f]. If there are multiple expressions on
+the right-hand side of a relation, then all of them must be satisfied
+in order for that clause of the relation to be satisfied.
 
-Note that relations are assumed to always return the same results
-for the same inputs, and their results are cached, unless
+Note that relations are assumed to always return the same results for
+the same inputs, and their results are cached, unless
 @scheme[caching-enable?] is set to @scheme[#f]. Accordingly, if a
-metafunction is called with the same inputs twice, then its body is
-only evaluated a single time.
+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?))]{