diff --git a/collects/redex/private/matcher.ss b/collects/redex/private/matcher.ss
index 64016610fe..0445b6ff51 100644
--- a/collects/redex/private/matcher.ss
+++ b/collects/redex/private/matcher.ss
@@ -612,7 +612,7 @@ before the pattern compiler is invoked.
        (mtch-context match)
        (mtch-hole match)))))
 
-;; compile-pattern : compiled-lang pattern boolean (listof sym) -> compiled-pattern
+;; compile-pattern : compiled-lang pattern boolean -> compiled-pattern
 (define (compile-pattern clang pattern bind-names?)
   (let-values ([(pattern has-hole?) (compile-pattern/cross? clang pattern #t bind-names?)])
     (make-compiled-pattern pattern)))
diff --git a/collects/redex/private/reduction-semantics.ss b/collects/redex/private/reduction-semantics.ss
index 55a7978a09..33988ee103 100644
--- a/collects/redex/private/reduction-semantics.ss
+++ b/collects/redex/private/reduction-semantics.ss
@@ -126,21 +126,25 @@
      lang
      (map
       (λ (make-proc)
-        (λ (lang)
-          (let ([f (make-proc lang)])
-            (λ (main-exp exp extend acc)
-              (let loop ([ms (or (match-pattern cp exp) '())]
-                         [acc acc])
-                (cond
-                  [(null? ms) acc]
-                  [else
-                   (let* ([mtch (car ms)]
-                          [bindings (mtch-bindings mtch)])
-                     (loop (cdr ms)
-                           (f main-exp
-                              (lookup-binding bindings 'exp)
-                              (λ (x) (extend (plug (lookup-binding bindings 'ctxt) x)))
-                              acc)))]))))))
+        (make-rewrite-proc
+         (λ (lang)
+           (let ([f (make-proc lang)])
+             (λ (main-exp exp extend acc)
+               (let loop ([ms (or (match-pattern cp exp) '())]
+                          [acc acc])
+                 (cond
+                   [(null? ms) acc]
+                   [else
+                    (let* ([mtch (car ms)]
+                           [bindings (mtch-bindings mtch)])
+                      (loop (cdr ms)
+                            (f main-exp
+                               (lookup-binding bindings 'exp)
+                               (λ (x) (extend (plug (lookup-binding bindings 'ctxt) x)))
+                               acc)))])))))
+         (rewrite-proc-name make-proc)
+         (rewrite-proc-lhs make-proc)
+         (rewrite-proc-id make-proc)))
       (reduction-relation-make-procs red))
      (reduction-relation-rule-names red)
      (reduction-relation-lws red)
@@ -200,16 +204,10 @@
 (define-syntax-set (do-reduction-relation)
   (define (do-reduction-relation/proc stx)
     (syntax-case stx ()
-      [(_ id orig-reduction-relation allow-zero-rules? lang w/domain-args ...)
+      [(_ id orig-reduction-relation allow-zero-rules? lang . w/domain-args)
        (identifier? #'lang)
-       (let-values ([(args domain-pattern)
-                     (syntax-case #'(w/domain-args ...) ()
-                       ;; commented out this case to diable domain specifications
-                       #;
-                       [(#:domain pat args ...)
-                        (values (syntax (args ...)) #'pat)]
-                       [else
-                        (values (syntax (w/domain-args ...)) #'any)])])
+       (let-values ([(domain-pattern main-arrow args)
+                     (parse-keywords stx #'id #'w/domain-args)])
          (with-syntax ([(rules ...) (before-with args)]
                        [(shortcuts ...) (after-with args)])
            (with-syntax ([(lws ...) (map rule->lws (syntax->list #'(rules ...)))])
@@ -229,6 +227,51 @@
                            stx 
                            #'lang)]))
   
+  (define (parse-keywords stx id args)
+    (let ([domain-contract #'any]
+          [default-arrow #'-->])
+      
+      ;; ensure no duplicate keywords
+      (let ([ht (make-hash)]
+            [known-keywords '(#;#:arrow #:domain)])  ;; #:arrow not yet implemented
+        (for-each (λ (kwd/stx)  ;; (not necc a keyword)
+                    (let ([kwd (syntax-e kwd/stx)])
+                      (when (keyword? kwd)
+                        (unless (member kwd known-keywords)
+                          (raise-syntax-error (syntax-e id)
+                                              "unknown keyword"
+                                              stx
+                                              kwd/stx))
+                        (when (hash-ref ht kwd #f)
+                          (raise-syntax-error (syntax-e id)
+                                              "duplicate keywords"
+                                              stx
+                                              kwd/stx
+                                              (list (hash-ref ht kwd))))
+                        (hash-set! ht kwd kwd/stx))))
+                  (syntax->list args)))
+      
+      (let loop ([args args])
+        (syntax-case args ()
+          [(#:domain pat args ...)
+           (begin (set! domain-contract #'pat)
+                  (loop #'(args ...)))]
+          [(#:domain)
+           (raise-syntax-error (syntax-e id) 
+                               "expected a domain after #:domain"
+                               stx)]
+          [(#:arrow arrow . args)
+           (begin (set! default-arrow #'arrow)
+                  (loop #'args))]
+          [(#:arrow)
+           (raise-syntax-error (syntax-e id) 
+                               "expected an arrow after #:arrow"
+                               stx)]
+          [_
+           (begin
+             (values domain-contract default-arrow args))]))))
+
+  
   (define (before-with stx)
     (let loop ([lst (syntax->list stx)])
       (cond
@@ -337,7 +380,10 @@
                                          (to-lw where-expr))
                                    ...))))]))
   
-  (define (reduction-relation/helper stx orig-name orig-red-expr lang-id rules shortcuts lws allow-zero-rules? domain-pattern)
+  (define (reduction-relation/helper stx orig-name orig-red-expr lang-id rules shortcuts 
+                                     lws 
+                                     allow-zero-rules?
+                                     domain-pattern)
     (let ([ht (make-module-identifier-mapping)]
           [all-top-levels '()]
           [withs (make-module-identifier-mapping)])
@@ -399,7 +445,8 @@
       (let ([name-ht (make-hasheq)]
             [lang-nts (language-id-nts lang-id orig-name)])
         (with-syntax ([lang-id lang-id]
-                      [(top-level ...) (get-choices stx orig-name ht lang-id (syntax -->) name-ht lang-id allow-zero-rules?)]
+                      [(top-level ...) (get-choices stx orig-name ht lang-id (syntax -->)
+                                                    name-ht lang-id allow-zero-rules?)]
                       [(rule-names ...) (hash-map name-ht (λ (k v) k))]
                       [lws lws]
                       
@@ -407,7 +454,7 @@
                        (rewrite-side-conditions/check-errs
                         lang-nts
                         orig-name
-                        #t
+                        #f
                         domain-pattern)])
                       
           #`(build-reduction-relation
@@ -789,8 +836,6 @@
      (reduction-relation-make-procs relation))
     (make-coverage h)))
 
-;(define fresh-coverage (compose make-coverage make-hasheq))
-
 (define (do-leaf-match name pat w/extras proc)
   (let ([case-id (gensym)])
     (make-rewrite-proc
diff --git a/collects/redex/private/struct.ss b/collects/redex/private/struct.ss
index f0c4e9d9f1..569a0c82d1 100644
--- a/collects/redex/private/struct.ss
+++ b/collects/redex/private/struct.ss
@@ -1,5 +1,7 @@
 #lang scheme/base
 
+(require "matcher.ss")
+
 ;; don't provide reduction-relation directly, so that we can use that for the macro's name.
 (provide reduction-relation-lang
          reduction-relation-make-procs
@@ -20,7 +22,9 @@
 ;;   we want to avoid doing it multiple times, so it is cached in a reduction-relation struct
 
 
-(define-values (make-rewrite-proc rewrite-proc? rewrite-proc-name rewrite-proc-lhs rewrite-proc-id)
+(define-values (make-rewrite-proc 
+                rewrite-proc? 
+                rewrite-proc-name rewrite-proc-lhs rewrite-proc-id)
   (let ()
     (define-values (type constructor predicate accessor mutator) 
       (make-struct-type 'rewrite-proc #f 4 0 #f '() #f 0))
@@ -45,19 +49,44 @@
 ;; the domain pattern isn't actually used here.
 ;; I started to add it, but didn't finish. -robby
 (define (build-reduction-relation orig-reduction-relation lang make-procs rule-names lws domain-pattern)
-  (cond
-    [orig-reduction-relation
-     (let* ([new-names (map rewrite-proc-name make-procs)]
-            [all-make-procs
-             (append (filter (λ (x) (or (not (rewrite-proc-name x))
-                                        (not (member (rewrite-proc-name x) new-names))))
-                             (reduction-relation-make-procs orig-reduction-relation))
-                     make-procs)])
-       (make-reduction-relation lang 
-                                all-make-procs
-                                (append (reduction-relation-rule-names orig-reduction-relation)
-                                        rule-names)
-                                lws ;; only keep new lws for typesetting
-                                (map (λ (make-proc) (make-proc lang)) all-make-procs)))]
-    [else
-     (make-reduction-relation lang make-procs rule-names lws (map (λ (make-proc) (make-proc lang)) make-procs))]))
+  (let* ([make-procs/check-domain
+          (map (λ (make-proc)
+                 (make-rewrite-proc
+                  (λ (lang)
+                    (let ([compiled-domain-pat (compile-pattern lang domain-pattern #f)]
+                          [proc (make-proc lang)])
+                      (λ (tl-exp exp f acc)
+                        (unless (match-pattern compiled-domain-pat tl-exp)
+                          (error 'reduction-relation "relation not defined for ~s" tl-exp))
+                        (let ([ress (proc tl-exp exp f acc)])
+                          (for-each
+                           (λ (res)
+                             (let ([term (cadr res)])
+                               (unless (match-pattern compiled-domain-pat term)
+                                 (error 'reduction-relation "relation reduced to ~s, which is outside its domain"
+                                        term))))
+                           ress)
+                          ress))))
+                  (rewrite-proc-name make-proc)
+                  (rewrite-proc-lhs make-proc)
+                  (rewrite-proc-id make-proc)))
+               make-procs)])
+    (cond
+      [orig-reduction-relation
+       (let* ([new-names (map rewrite-proc-name make-procs)]
+              [all-make-procs
+               (append
+                (filter (λ (x) (or (not (rewrite-proc-name x))
+                                   (not (member (rewrite-proc-name x) new-names))))
+                        (reduction-relation-make-procs orig-reduction-relation))
+                make-procs/check-domain)])
+         (make-reduction-relation lang 
+                                  all-make-procs
+                                  (append (reduction-relation-rule-names orig-reduction-relation)
+                                          rule-names)
+                                  lws ;; only keep new lws for typesetting
+                                  (map (λ (make-proc) (make-proc lang)) all-make-procs)))]
+      [else
+       (make-reduction-relation lang make-procs/check-domain rule-names lws 
+                                (map (λ (make-proc) (make-proc lang)) 
+                                     make-procs/check-domain))])))
diff --git a/collects/redex/private/tl-test.ss b/collects/redex/private/tl-test.ss
index 049dda3d01..02e7d79d1d 100644
--- a/collects/redex/private/tl-test.ss
+++ b/collects/redex/private/tl-test.ss
@@ -750,6 +750,99 @@
          '(p q r))
         (list '((p q r))))
 
+  #;
+  (test (apply-reduction-relation
+         (reduction-relation 
+          empty-language
+          #:main-arrow :->
+          (:-> 1 2))
+         1)
+        '(2))
+  
+  (test (apply-reduction-relation
+         (reduction-relation 
+          empty-language
+          #:domain number
+          (--> 1 2))
+         1)
+        '(2))
+  
+  
+  (test (let ([red
+               (reduction-relation 
+                empty-language
+                #:domain number
+                (--> 1 2))])
+          (with-handlers ((exn? exn-message))
+            (apply-reduction-relation red 'x)
+            'no-exception-raised))
+        "reduction-relation: relation not defined for x")
+
+  (test (let ([red
+               (reduction-relation 
+                empty-language
+                #:domain number
+                (--> 1 x))])
+          (with-handlers ((exn? exn-message))
+            (apply-reduction-relation red 1)
+            'no-exception-raised))
+        "reduction-relation: relation reduced to x, which is outside its domain")
+
+  (let* ([red1
+          (reduction-relation 
+           empty-language
+           #:domain (side-condition number_1 (even? (term number_1)))
+           (--> number number))]
+         [red2
+          (reduction-relation 
+           empty-language
+           #:domain (side-condition number_1 (odd? (term number_1)))
+           (--> number number))]
+         [red-c
+          (union-reduction-relations red1 red2)])
+    
+    ;; ensure first branch of 'union' is checked  
+    (test (with-handlers ((exn? exn-message))
+            (apply-reduction-relation red-c 1)
+            'no-exception-raised)
+          "reduction-relation: relation not defined for 1")
+
+    ;; ensure second branch of 'union' is checked
+    (test (with-handlers ((exn? exn-message))
+            (apply-reduction-relation red-c 2)
+            'no-exception-raised)
+          "reduction-relation: relation not defined for 2"))
+
+  (let ()
+    (define-language l1
+      (D 0 1 2))
+    (define r1
+      (reduction-relation 
+       l1
+       #:domain D
+       (--> D D)))
+    (define-language l2
+      (D 0 1 2 3))
+    (define r2
+      (extend-reduction-relation r1 l2))
+    
+    ;; test that the domain is re-interpreted for the extended reduction-relation
+    (test (apply-reduction-relation r2 3)
+          '(3)))
+  
+  (let ()
+    (define-language l1
+      (D 0 1 2))
+    (define r1
+      (reduction-relation 
+       l1
+       #:domain (D D)
+       (--> (D_1 D_2) (D_2 D_1))))
+    
+    ;; test that duplicated identifiers in the domain contract do not have to be equal
+    (test (apply-reduction-relation r1 (term (1 2)))
+          (list (term (2 1)))))
+  
   (parameterize ([current-namespace syn-err-test-namespace])
     (eval (quote-syntax
            (define-language grammar
diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl
index ddacfc7c34..edb4374dfb 100644
--- a/collects/redex/redex.scrbl
+++ b/collects/redex/redex.scrbl
@@ -638,15 +638,16 @@ all non-GUI portions of Redex) and also exported by
 @schememodname[redex] (which includes all of Redex).
 
 @defform/subs[#:literals (--> fresh side-condition where) 
-              (reduction-relation language reduction-case ...)
-              ([reduction-case (--> #, @|ttpattern| #, @|tttterm| extras ...)]
+              (reduction-relation language domain reduction-case ...)
+              ([domain (code:line) (code:line #:domain #, @|ttpattern|)]
+               [reduction-case (--> #, @|ttpattern| #, @|tttterm| extras ...)]
                [extras name
                        (fresh fresh-clause ...)
                        (side-condition scheme-expression ...)
                        (where tl-pat #, @|tttterm|)]
-                [fresh-clause var ((var1 ...) (var2 ...))]
-                [tl-pat identifier (tl-pat-ele ...)]
-                [tl-pat-ele tl-pat (code:line tl-pat ... (code:comment "a literal ellipsis"))])]{
+               [fresh-clause var ((var1 ...) (var2 ...))]
+               [tl-pat identifier (tl-pat-ele ...)]
+               [tl-pat-ele tl-pat (code:line tl-pat ... (code:comment "a literal ellipsis"))])]{
 
 Defines a reduction relation casewise, one case for each of the
 clauses beginning with @scheme[-->]. Each of the @scheme[pattern]s