diff --git a/collects/redex/examples/delim-cont/reduce.rkt b/collects/redex/examples/delim-cont/reduce.rkt
index 4ef453e5b0..c1f909545b 100644
--- a/collects/redex/examples/delim-cont/reduce.rkt
+++ b/collects/redex/examples/delim-cont/reduce.rkt
@@ -112,8 +112,8 @@
    ;;  thunk and then tries again to invoke the continuation --- but inside a
    ;;  `dw' for the already-run pre-thunk, so that it's treated as shared and not
    ;;  run again.
-   (~~> (% v_1 (in-hole D_2 (in-hole W_3 ((cont v_1 (name k_1 (in-hole D_6 (in-hole W_4 (dw x_1 e_1 (hide-hole E_5) e_2))))) v_2))) v_3)
-        (% v_1 (in-hole D_6 (in-hole W_4 (begin e_1 (dw x_1 e_1 ((cont v_1 k_1) v_2) e_2)))) v_3)
+   (~~> (% v_1 (in-hole D_2 (in-hole W_3 ((cont v_1 (name k (in-hole D_6 (in-hole W_4 (dw x_1 e_1 (hide-hole E_5) e_2))))) v_2))) v_3)
+        (% v_1 (in-hole D_6 (in-hole W_4 (begin e_1 (dw x_1 e_1 ((cont v_1 k) v_2) e_2)))) v_3)
         (side-condition (term (noMatch (in-hole D_2 W_3) E (% v_1 E v))))
         (side-condition (term (sameDWs D_2 D_6)))
         (side-condition (term (noShared W_3 (in-hole W_4 (dw x_1 e_1 E_5 e_2)))))
diff --git a/collects/redex/examples/racket-machine/util.rkt b/collects/redex/examples/racket-machine/util.rkt
index a582c5e630..4c008d8b79 100644
--- a/collects/redex/examples/racket-machine/util.rkt
+++ b/collects/redex/examples/racket-machine/util.rkt
@@ -5,12 +5,12 @@
 
 (provide (all-defined-out))
 
-(define-language any)
+(define-language any-L)
 
-(define-metafunction any
+(define-metafunction any-L
   [(count-up number)
    ,(build-list (term number) (λ (x) x))])
 
-(define-metafunction any
+(define-metafunction any-L
   concat : (any ...) ... -> (any ...)
   [(concat any ...) ,(apply append (term (any ...)))])
diff --git a/collects/redex/private/compiler/match.rkt b/collects/redex/private/compiler/match.rkt
index 7b72a8036e..fe298581bf 100644
--- a/collects/redex/private/compiler/match.rkt
+++ b/collects/redex/private/compiler/match.rkt
@@ -907,40 +907,40 @@
                          bool))
         (in-hole Context
                  (letrec ((match-repeat
-                           (λ (z binding_temp ... bound_temp ...)      
+                           (λ (z any_binding_temp ... any_bound_temp ...)      
                              (begin
-                               (when (and (null? bound_temp) ...)
+                               (when (and (null? any_bound_temp) ...)
                                  (Build-Let ;reverse
-                                  (let ([pvar_11 binding_temp] ...)
+                                  (let ([pvar_11 any_binding_temp] ...)
                                     (matrix (z x_2 ...)
-                                            (((p_4 p_5 ... -> r_2) ,@(term (Add-Repeat-Vars (eqs_2 ...) (pvar_11 ...) (binding_temp ...)))))
-                                            (((Get-Pvar pvar_22) bound_temp) ...)
+                                            (((p_4 p_5 ... -> r_2) ,@(term (Add-Repeat-Vars (eqs_2 ...) (pvar_11 ...) (any_binding_temp ...)))))
+                                            (((Get-Pvar pvar_22) any_bound_temp) ...)
                                             (pvar_3 ...) ; fix this
                                             natural
                                             bool))
-                                  (binding_temp ...)))
-                               (when (and (cons? z) (cons? bound_temp) ...)
+                                  (any_binding_temp ...)))
+                               (when (and (cons? z) (cons? any_bound_temp) ...)
                                  (let ((carz (car z))
-                                       (car_bound_temp (car bound_temp))
+                                       (any_car_bound_temp (car any_bound_temp))
                                        ...)
                                    (matrix (carz)
                                            (((p_3 -> (match-repeat 
                                                       (cdr z)
-                                                      (cons pvar_11 binding_temp) ...
-                                                      (cdr bound_temp) ...))
+                                                      (cons pvar_11 any_binding_temp) ...
+                                                      (cdr any_bound_temp) ...))
                                              eqs_2 ...))
-                                           (((Get-Pvar pvar_22) car_bound_temp) ...)
+                                           (((Get-Pvar pvar_22) any_car_bound_temp) ...)
                                            (pvar_3 ...)
                                            ,(+ 1 (term natural))
                                            bool))
                                  )))))
                    (Build-Temp-Let natural
-                                   (bound_temp ...) 
+                                   (any_bound_temp ...) 
                                    (pvar_22 ...)
-                                   (Build-Let-Empty natural ,(map (λ (x) (term (Get-Pvar ,x))) (term (binding_temp ...)))
+                                   (Build-Let-Empty natural ,(map (λ (x) (term (Get-Pvar ,x))) (term (any_binding_temp ...)))
                                                     ;,(if (zero? (term natural))
-                                                    (match-repeat x_1 binding_temp ... bound_temp ...)
-                                                    ;(term (match-repeat x_1 binding_temp ... (car bound_temp) ...))
+                                                    (match-repeat x_1 any_binding_temp ... any_bound_temp ...)
+                                                    ;(term (match-repeat x_1 any_binding_temp ... (car any_bound_temp) ...))
                                                     ;)
                                                     )
                                    )
@@ -958,13 +958,13 @@
         (fresh match-repeat)
         (fresh z)
         (fresh carz)
-        (fresh ((binding_temp ...)
+        (fresh ((any_binding_temp ...)
                 (pvar_11 ...)))
         (fresh ((single_binding_temp ...)
                 (pvar_11 ...)))
-        (fresh ((bound_temp ...)
+        (fresh ((any_bound_temp ...)
                 (pvar_22 ...)))
-        (fresh ((car_bound_temp ...)
+        (fresh ((any_car_bound_temp ...)
                 (pvar_22 ...)))
         (side-condition (not (term (Flushable? 
                                     (eqs_2 ...)))))
diff --git a/collects/redex/private/judgment-form.rkt b/collects/redex/private/judgment-form.rkt
index 400a430d48..d149226205 100644
--- a/collects/redex/private/judgment-form.rkt
+++ b/collects/redex/private/judgment-form.rkt
@@ -105,7 +105,8 @@
                           lang-nts
                           'reduction-relation
                           #t
-                          #'x)])
+                          #'x)]
+                        [lang-stx lang])
             (define-values (binding-constraints temporaries env+)
               (generate-binding-constraints (syntax->list #'(names ...))
                                             (syntax->list #'(names/ellipses ...))
@@ -120,7 +121,7 @@
                      [(predicate)
                       #'combine-where-results/predicate]
                      [else (error 'unknown-where-mode "~s" where-mode)])
-                 (match-pattern (compile-pattern #,lang `side-conditions-rewritten #t) (term e))
+                 (match-pattern (compile-pattern #,lang `side-conditions-rewritten #t) (term/nts e #,lang-nts))
                  (λ (bindings)
                    (let ([x (lookup-binding bindings 'names)] ...)
                      (and binding-constraints ...
@@ -184,7 +185,7 @@
                        (generate-binding-constraints output-names output-names/ellipses env orig-name)]
                       [(rest-body) (loop rest-clauses #`(list judgment-output #,to-not-be-in) env+)]
                       [(call)
-                       (let ([input (quasisyntax/loc premise (term #,input-template))])
+                       (let ([input (quasisyntax/loc premise (term/nts #,input-template #,lang-nts))])
                          (define (make-traced input)
                            (quasisyntax/loc premise
                              (call-judgment-form 'form-name #,judgment-proc '#,mode #,input)))
@@ -341,10 +342,10 @@
   (define definitions
     #`(begin
         (define-syntax #,judgment-form-name 
-          (judgment-form '#,judgment-form-name '#,(cdr (syntax->datum mode)) #'judgment-form-proc #'mk-judgment-form-proc #'#,lang #'judgment-form-lws))
+          (judgment-form '#,judgment-form-name '#,(cdr (syntax->datum mode)) #'judgment-form-runtime-proc #'mk-judgment-form-proc #'#,lang #'judgment-form-lws))
         (define mk-judgment-form-proc
           (compile-judgment-form-proc #,judgment-form-name #,mode #,lang #,clauses #,position-contracts #,orig #,stx #,syn-err-name))
-        (define judgment-form-proc (mk-judgment-form-proc #,lang))
+        (define judgment-form-runtime-proc (mk-judgment-form-proc #,lang))
         (define judgment-form-lws
           (compiled-judgment-form-lws #,clauses))))
   (syntax-property
@@ -353,7 +354,7 @@
         ; Introduce the names before using them, to allow
         ; judgment form definition at the top-level.
         #`(begin 
-            (define-syntaxes (judgment-form-proc judgment-form-lws) (values))
+            (define-syntaxes (judgment-form-runtime-proc judgment-form-lws) (values))
             #,definitions)
         definitions))
    'disappeared-use
@@ -455,7 +456,7 @@
             [judgment (syntax-case stx () [(_ judgment _) #'judgment])])
        (check-judgment-arity stx judgment)
        #`(sort #,(bind-withs syn-err-name '() lang nts (list judgment)
-                             'flatten #`(list (term #,#'tmpl)) '() '() #f)
+                             'flatten #`(list (term #,#'tmpl #:lang #,lang)) '() '() #f)
                string<=?
                #:key (λ (x) (format "~s" x))))]
     [(_ (not-form-name . _) . _)
@@ -492,7 +493,7 @@
                                    (struct-copy judgment-form (lookup-judgment-form-id name)
                                                 [proc #'recur]))])
                (bind-withs syn-error-name '() #'lang nts (syntax->list #'prems) 
-                           'flatten #`(list (term (#,@output-pats))) 
+                           'flatten #`(list (term/nts (#,@output-pats) #,nts)) 
                            (syntax->list #'(names ...))
                            (syntax->list #'(names/ellipses ...))
                            #f)))
diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt
index 19f86b23be..ae75ce496d 100644
--- a/collects/redex/private/reduction-semantics.rkt
+++ b/collects/redex/private/reduction-semantics.rkt
@@ -662,7 +662,7 @@
                  (λ (bindings rhs-binder)
                    (term-let ([lhs-to-id rhs-binder]
                               [names/ellipses (lookup-binding bindings 'names)] ...)
-                             (term rhs-to)))
+                             (term rhs-to #:lang lang)))
                  #,child-proc
                  `fresh-rhs-from))
             (get-choices stx orig-name bm #'lang
@@ -721,7 +721,7 @@
                         sides/withs/freshs
                         'flatten
                         #`(list (cons #,(or computed-name #'none)
-                                      (term #,to)))
+                                      (term #,to #:lang #,lang)))
                         (syntax->list #'(names ...))
                         (syntax->list #'(names/ellipses ...))
                         #t))
@@ -1243,7 +1243,7 @@
                                     syn-error-name '()  
                                     #'effective-lang lang-nts
                                     sc/b 'flatten
-                                    #`(list (term #,rhs))
+                                    #`(list (term #,rhs #:lang lang))
                                     (syntax->list names) 
                                     (syntax->list names/ellipses)
                                     #t))
diff --git a/collects/redex/private/rewrite-side-conditions.rkt b/collects/redex/private/rewrite-side-conditions.rkt
index 7055436cf2..414ae8d6fa 100644
--- a/collects/redex/private/rewrite-side-conditions.rkt
+++ b/collects/redex/private/rewrite-side-conditions.rkt
@@ -3,6 +3,7 @@
   (require mzlib/list
            "underscore-allowed.rkt")
   (require "term.rkt"
+           "term-fn.rkt"
            setup/path-to-relative
            (for-template
             mzscheme
@@ -18,18 +19,6 @@
   
   (provide (struct-out id/depth))
   
-  (define-values (language-id make-language-id language-id? language-id-get language-id-set) (make-struct-type 'language-id #f 2 0 #f '() #f 0))
-  
-  (define (language-id-nts stx id) (language-id-getter stx id 1))
-  (define (language-id-getter stx id n)
-    (unless (identifier? stx)
-      (raise-syntax-error id "expected an identifier defined by define-language" stx))
-    (let ([val (syntax-local-value stx (λ () #f))])
-      (unless (and (set!-transformer? val)
-                   (language-id? (set!-transformer-procedure val)))
-        (raise-syntax-error id "expected an identifier defined by define-language" stx))
-      (language-id-get (set!-transformer-procedure val) n)))
-  
   (define (rewrite-side-conditions/check-errs all-nts what bind-names? orig-stx)
     (define (expected-exact name n stx)
       (raise-syntax-error what (format "~a expected to have ~a arguments" 
diff --git a/collects/redex/private/term-fn.rkt b/collects/redex/private/term-fn.rkt
index da2e0683cb..37d03a400b 100644
--- a/collects/redex/private/term-fn.rkt
+++ b/collects/redex/private/term-fn.rkt
@@ -11,7 +11,10 @@
          (struct-out defined-term)
          defined-term-id?
          defined-check
-         not-expression-context)
+         not-expression-context
+         make-language-id
+         language-id-nts
+         pattern-symbols)
 
 (define-values (struct-type make-term-fn term-fn? term-fn-get term-fn-set!) 
   (make-struct-type 'term-fn #f 1 0))
@@ -38,3 +41,18 @@
 (define (not-expression-context stx)
   (when (eq? (syntax-local-context) 'expression)
     (raise-syntax-error #f "not allowed in an expression context" stx)))
+
+(define-values (language-id make-language-id language-id? language-id-get language-id-set) (make-struct-type 'language-id #f 2 0 #f '() #f 0))
+
+(define (language-id-nts stx id) (language-id-getter stx id 1))
+(define (language-id-getter stx id n)
+  (unless (identifier? stx)
+    (raise-syntax-error id "expected an identifier defined by define-language" stx))
+  (let ([val (syntax-local-value stx (λ () #f))])
+    (unless (and (set!-transformer? val)
+                 (language-id? (set!-transformer-procedure val)))
+      (raise-syntax-error id "expected an identifier defined by define-language" stx))
+    (language-id-get (set!-transformer-procedure val) n)))
+
+(define pattern-symbols '(any number natural integer real string variable 
+                              variable-not-otherwise-mentioned hole symbol))
diff --git a/collects/redex/private/term.rkt b/collects/redex/private/term.rkt
index ec3c500689..c420d755dd 100644
--- a/collects/redex/private/term.rkt
+++ b/collects/redex/private/term.rkt
@@ -4,14 +4,17 @@
                      "term-fn.rkt"
                      syntax/boundmap
                      syntax/parse
-                     racket/syntax)
+                     racket/syntax
+                     "keyword-macros.rkt"
+                     "matcher.rkt")
          syntax/datum
          "error.rkt"
          "matcher.rkt")
 
 (provide term term-let define-term
          hole in-hole
-         term-let/error-name term-let-fn term-define-fn)
+         term-let/error-name term-let-fn term-define-fn
+         term/nts)
 
 (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"))
@@ -21,14 +24,37 @@
     [(_ () e) (syntax e)]
     [(_ (a b ...) e) (syntax (with-syntax (a) (with-syntax* (b ...) e)))]))
 
-(define-syntax-rule (term t)
-  (#%expression (term/private t)))
+(define-for-syntax lang-keyword
+  (list '#:lang #f))
+
+(define-syntax (term stx)
+  (syntax-case stx ()
+    [(term t . kw-args)
+     (with-syntax ([(lang-stx) (parse-kw-args (list lang-keyword)
+                                                 (syntax kw-args)
+                                                 stx
+                                                 (syntax-e #'form))])
+       (if (syntax->datum #'lang-stx)
+           (let ([lang-nts (language-id-nts #'lang-stx 'term)])
+             #`(term/nts t #,lang-nts))
+           #'(term/nts t #f)))]))
+
+(define-syntax (term/nts stx)
+  (syntax-case stx ()
+    [(_ arg nts)
+     #'(#%expression (term/private arg nts))]))
 
 (define-syntax (term/private orig-stx)
+  (define lang-nts #f)
   (define outer-bindings '())
   (define applied-metafunctions
     (make-free-identifier-mapping))
   
+  (define error-stx
+    (syntax-case orig-stx ()
+      [(_ e-stx nts-stx)
+       #'e-stx]))
+  
   (define (rewrite stx)
     (let-values ([(rewritten _) (rewrite/max-depth stx 0)])
       rewritten))
@@ -71,6 +97,7 @@
        (and (identifier? (syntax x))
             (term-id? (syntax-local-value (syntax x) (λ () #f))))
        (let ([id (syntax-local-value/record (syntax x) (λ (x) #t))])
+         (check-id (syntax->datum (term-id-id id)) stx)
          (values (datum->syntax (term-id-id id) (syntax-e (term-id-id id)) (syntax x))
                  (term-id-depth id)))]
       [x
@@ -78,6 +105,7 @@
        (let ([ref (syntax-property
                    (defined-term-value (syntax-local-value #'x))
                    'disappeared-use #'x)])
+         (check-id (syntax->datum #'x) stx)
          (with-syntax ([v #`(begin
                               #,(defined-check ref "term" #:external #'x)
                               #,ref)])
@@ -95,6 +123,10 @@
       [(in-hole . x)
        (raise-syntax-error 'term "malformed in-hole" orig-stx stx)]
       [hole (values (syntax (undatum the-hole)) 0)]
+      [x
+       (and (identifier? (syntax x))
+            (check-id (syntax->datum #'x) stx))
+       (values stx 0)]
       
       
       [() (values stx 0)]
@@ -121,22 +153,32 @@
       
       [_ (values stx 0)]))
   
+  (define (check-id id stx)
+    (when lang-nts
+      (define m (regexp-match #rx"^([^_]*)_" (symbol->string id)))
+      (when m
+        (unless (memq (string->symbol (list-ref m 1)) (append pattern-symbols lang-nts))
+          (raise-syntax-error 'term "before underscore must be either a non-terminal or a built-in pattern" error-stx stx)))))
+  
   (syntax-case orig-stx ()
-    [(_ arg)
-     (with-disappeared-uses
-      (with-syntax ([rewritten (rewrite (syntax arg))])
-        #`(begin
-            #,@(free-identifier-mapping-map
-                applied-metafunctions
-                (λ (f _) (defined-check f "metafunction")))
-            #,(let loop ([bs (reverse outer-bindings)])
-                (cond
-                  [(null? bs) (syntax (quasidatum rewritten))]
-                  [else (with-syntax ([rec (loop (cdr bs))]
-                                      [fst (car bs)])
-                          (syntax (with-datum (fst)
-                                    rec)))])))))]))
-
+    [(_ arg nts-stx)
+     (begin
+       (when (syntax->datum #'nts-stx)
+         (set! lang-nts (syntax->datum #'nts-stx)))
+       (with-disappeared-uses
+        (with-syntax ([rewritten (rewrite (syntax arg))])
+          #`(begin
+              #,@(free-identifier-mapping-map
+                  applied-metafunctions
+                  (λ (f _) (defined-check f "metafunction")))
+              #,(let loop ([bs (reverse outer-bindings)])
+                  (cond
+                    [(null? bs) (syntax (quasidatum rewritten))]
+                    [else (with-syntax ([rec (loop (cdr bs))]
+                                        [fst (car bs)])
+                            (syntax (with-datum (fst)
+                                                rec)))]))))))]))
+ 
 (define-syntax (term-let-fn stx)
   (syntax-case stx ()
     [(_ ([f rhs] ...) body1 body2 ...)
diff --git a/collects/redex/scribblings/ref.scrbl b/collects/redex/scribblings/ref.scrbl
index b8afcb0ece..59784d265f 100644
--- a/collects/redex/scribblings/ref.scrbl
+++ b/collects/redex/scribblings/ref.scrbl
@@ -450,9 +450,9 @@ them.}
 produces the boolean or the string.}
 ]
 
-@defform[(term @#,tttterm)]{
+@defform*[[(term @#,tttterm) (term @#,tttterm #:lang lang-id)]]{
 
-This form is used for construction of a term.
+Used for construction of a term.
 
 It behaves similarly to @racket[quasiquote], except for a few special
 forms that are recognized (listed below) and that names bound by
@@ -460,6 +460,16 @@ forms that are recognized (listed below) and that names bound by
 those names were bound to, expanding ellipses as in-place sublists (in
 the same manner as syntax-case patterns).
 
+The optional @racket[#:lang] keyword must supply an identifier bound
+by @racket[define-language], and adds a check that any symbol containing
+an underscore in @tttterm could have been bound by a pattern in the
+language referenced by @racket[lang-id].  In practice, this means that the
+underscore must be preceded by a non-terminal in that langauge or a
+built-in @ttpattern such as @racket[number].  This form of @racket[term]
+is used internally by default, so this check is applied to terms 
+that are constructed by Redex forms such as @racket[reduction-relation] 
+and @racket[define-metafunction].
+
 For example,
 
 @racketblock[
diff --git a/collects/redex/tests/rg-test.rkt b/collects/redex/tests/rg-test.rkt
index 0a17a6be40..9602345cd2 100644
--- a/collects/redex/tests/rg-test.rkt
+++ b/collects/redex/tests/rg-test.rkt
@@ -1201,12 +1201,12 @@
     (define-extended-language M L (x 2))
     (define-metafunction L 
       [(f)
-       _
+       ?
        (where x 2)])
     (define-metafunction/extension f M
       g : any -> any)
     (test (with-handlers ([exn:fail:redex:generation-failure? (const #f)])
-            (check-metafunction g (λ (_) #t) #:attempts 1 #:print? #f))
+            (check-metafunction g (λ (?) #t) #:attempts 1 #:print? #f))
           #t))
   
   (test (output (λ () (check-metafunction m (λ (_) #t)))) #rx"no counterexamples")
diff --git a/collects/redex/tests/syn-err-tests/metafunction-definition.rktd b/collects/redex/tests/syn-err-tests/metafunction-definition.rktd
index f2ef21b61a..50824e18e6 100644
--- a/collects/redex/tests/syn-err-tests/metafunction-definition.rktd
+++ b/collects/redex/tests/syn-err-tests/metafunction-definition.rktd
@@ -18,3 +18,9 @@
 (#rx"expected an identifier"
  ([not-id junk])
  (define-metafunction not-id also-junk))
+
+(#rx"before underscore"
+ ([not-non-term z!_1])
+ (define-metafunction syn-err-lang
+  [(func M_1 E_2)
+   (M_1 (E_2 not-non-term) M_1)]))
diff --git a/collects/redex/tests/syn-err-tests/reduction-relation-definition.rktd b/collects/redex/tests/syn-err-tests/reduction-relation-definition.rktd
index cff6dff1bf..292aa1937b 100644
--- a/collects/redex/tests/syn-err-tests/reduction-relation-definition.rktd
+++ b/collects/redex/tests/syn-err-tests/reduction-relation-definition.rktd
@@ -136,3 +136,10 @@
     syn-err-lang
     (--> 1 1
          (judgment-holds bad-judgment)))))
+
+(#rx"before underscore"
+ ([not-non-term Z_1])
+ (reduction-relation 
+  syn-err-lang
+  (--> (in-hole E (Q_1 M_1))
+       (in-hole E (M_1 not-non-term)))))
diff --git a/collects/redex/tests/syn-err-tests/term-lang.rktd b/collects/redex/tests/syn-err-tests/term-lang.rktd
new file mode 100644
index 0000000000..ccf298440f
--- /dev/null
+++ b/collects/redex/tests/syn-err-tests/term-lang.rktd
@@ -0,0 +1,7 @@
+(#rx"before underscore"
+ ([not-a-non-term Z_1])
+ (term not-a-non-term #:lang syn-err-lang))
+
+(#rx"before underscore"
+ ([not-a-non-term AA_1])
+ (term (Q_1 Q_2 (Q_3 not-a-non-term)) #:lang syn-err-lang))
diff --git a/collects/redex/tests/tl-test.rkt b/collects/redex/tests/tl-test.rkt
index af35d28cbf..c51ee87754 100644
--- a/collects/redex/tests/tl-test.rkt
+++ b/collects/redex/tests/tl-test.rkt
@@ -435,6 +435,25 @@
     (exec-runtime-error-tests "run-err-tests/define-union-language.rktd"))
   
   (exec-syntax-error-tests "syn-err-tests/language-definition.rktd")
+  
+  ;; term with #:lang tests
+  (exec-syntax-error-tests "syn-err-tests/term-lang.rktd")
+  
+  (let ()
+    (define-language L
+      (a number)
+      (b (a a))
+      (c (b b)))
+    (test (term 1 #:lang L) 1)
+    (test (term ((1 2) (3 4)) #:lang L) '((1 2) (3 4)))
+    (test (term (1 2 3 4) #:lang L) '(1 2 3 4))
+    (test (redex-let L ([a_1 5])
+                     (term (a_1 6) #:lang L))
+          '(5 6))
+    (test (redex-let L ([number_1 5])
+                     (term (number_1 6) #:lang L))
+          '(5 6)))
+    
 ;                                                                                             
 ;                                                                                             
 ;                                 ;;;                                ;                        
diff --git a/doc/release-notes/redex/HISTORY.txt b/doc/release-notes/redex/HISTORY.txt
index 75db8643b5..28009462e7 100644
--- a/doc/release-notes/redex/HISTORY.txt
+++ b/doc/release-notes/redex/HISTORY.txt
@@ -1,3 +1,7 @@
+v5.3.1
+
+  * added optional #:lang keyword to term
+
 v5.3
 
   * added the amb tutorial.