diff --git a/collects/redex/HISTORY b/collects/redex/HISTORY
index 555d9a7a6a..7881397b20 100644
--- a/collects/redex/HISTORY
+++ b/collects/redex/HISTORY
@@ -6,6 +6,9 @@ v4.2
   - added render-* functions that make it easier to experiment
     with typesetting at the REPL.
 
+  - where clauses in metafunctions now are implicitly in
+    `term's (they were not documented at all before)
+
 v4.1 (this is the first version that was included in the PLT
       distribution. Before this, Redex was in PLaneT).
 
diff --git a/collects/redex/private/reduction-semantics.ss b/collects/redex/private/reduction-semantics.ss
index a4d3a466f6..6b33048507 100644
--- a/collects/redex/private/reduction-semantics.ss
+++ b/collects/redex/private/reduction-semantics.ss
@@ -781,6 +781,24 @@
     ((metafunc-proc-in-dom? mp)
      exp)))
 
+
+;                                                                                                          
+;                                                                                                          
+;                                                                                                          
+;                            ;              ;;;                                 ;    ;;                    
+;                           ;;             ;;;;                                ;;    ;;                    
+;  ;;;;;;; ;;;;    ;;;    ;;;;; ;;;;;;;   ;;;;; ;;;; ;;;; ;;;; ;;;    ;;;;;  ;;;;;        ;;;;   ;;;; ;;;  
+;  ;;;;;;;;;;;;;  ;;;;;  ;;;;;; ;;;;;;;;  ;;;;  ;;;; ;;;; ;;;;;;;;;  ;;;;;; ;;;;;; ;;;;  ;;;;;;  ;;;;;;;;; 
+;  ;;;; ;;; ;;;; ;;;; ;;  ;;;;      ;;;; ;;;;;; ;;;; ;;;; ;;;; ;;;; ;;;;;;;  ;;;;  ;;;; ;;;;;;;; ;;;; ;;;; 
+;  ;;;; ;;; ;;;; ;;;;;;;  ;;;;   ;;;;;;; ;;;;;; ;;;; ;;;; ;;;; ;;;; ;;;;     ;;;;  ;;;; ;;;; ;;; ;;;; ;;;; 
+;  ;;;; ;;; ;;;; ;;;;;    ;;;;; ;;  ;;;;  ;;;;  ;;;; ;;;; ;;;; ;;;; ;;;;;;;  ;;;;; ;;;; ;;;;;;;; ;;;; ;;;; 
+;  ;;;; ;;; ;;;;  ;;;;;;  ;;;;; ;;;;;;;;  ;;;;  ;;;;;;;;; ;;;; ;;;;  ;;;;;;  ;;;;; ;;;;  ;;;;;;  ;;;; ;;;; 
+;  ;;;; ;;; ;;;;   ;;;;    ;;;;  ;; ;;;;  ;;;;   ;;; ;;;; ;;;; ;;;;   ;;;;;   ;;;; ;;;;   ;;;;   ;;;; ;;;; 
+;                                                                                                          
+;                                                                                                          
+;                                                                                                          
+
+
 (define-syntax-set (define-metafunction define-metafunction/extension)
   
   (define (define-metafunction/proc stx)
@@ -858,7 +876,7 @@
                                              (syntax 
                                               (λ (name bindings)
                                                 (term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
-                                                          (term-let ([tl-var tl-exp] ...)
+                                                          (term-let ([tl-var (term tl-exp)] ...)
                                                                     (term-let-fn ((name name))
                                                                                  (term rhs)))))))))
                                        (syntax->list (syntax (lhs ...)))
diff --git a/collects/redex/private/size-snip.ss b/collects/redex/private/size-snip.ss
index 3d2ef658f7..9c81cf34ed 100644
--- a/collects/redex/private/size-snip.ss
+++ b/collects/redex/private/size-snip.ss
@@ -2,7 +2,8 @@
   (require (lib "mred.ss" "mred")
            (lib "class.ss")
            (lib "pretty.ss")
-           (lib "framework.ss" "framework"))
+           (lib "framework.ss" "framework")
+           "matcher.ss")
   
   (provide reflowing-snip<%>
            size-editor-snip%
@@ -13,7 +14,15 @@
   (define initial-char-width (make-parameter 30))
   
   (define (default-pretty-printer v port w spec)
-    (parameterize ([pretty-print-columns w])
+    (parameterize ([pretty-print-columns w]
+                   [pretty-print-size-hook
+                    (λ (val display? op)
+                      (cond
+                        [(hole? val) 4]
+                        [else #f]))]
+                   [pretty-print-print-hook
+                    (λ (val display? op)
+                      (display "hole" op))])
       (pretty-print v port)))
   
   (define reflowing-snip<%>
diff --git a/collects/redex/private/tl-test.ss b/collects/redex/private/tl-test.ss
index 7bf2f400ef..36dabcc339 100644
--- a/collects/redex/private/tl-test.ss
+++ b/collects/redex/private/tl-test.ss
@@ -397,9 +397,17 @@
     (define-metafunction empty-language
       [(f (number_1 number_2))
        number_3
-       (where number_3 (+ (term number_1) (term number_2)))])
+       (where number_3 ,(+ (term number_1) (term number_2)))])
     (test (term (f (11 17))) 28))
   
+  (let ()
+    (define-metafunction empty-language
+      [(f variable) 
+       (x x)
+       (where x (variable variable))])
+    (test (term (f z)) 
+          (term ((z z) (z z)))))
+  
   (let ()
     (define-language x-lang
       (x variable))
diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl
index b41ce93302..48f403ce86 100644
--- a/collects/redex/redex.scrbl
+++ b/collects/redex/redex.scrbl
@@ -607,12 +607,14 @@ all non-GUI portions of Redex) and also exported by
 
 @defform/subs[#:literals (--> fresh side-condition where) 
               (reduction-relation language reduction-case ...)
-              ((reduction-case (--> #, @|ttpattern| #, @|tttterm| extras ...))
-               (extras name
+              ([reduction-case (--> #, @|ttpattern| #, @|tttterm| extras ...)]
+               [extras name
                        (fresh fresh-clause ...)
                        (side-condition scheme-expression ...)
-                       (where tl-pat #, @|tttterm|))
-               (fresh-clause var ((var1 ...) (var2 ...))))]{
+                       (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"))])]{
 
 Defines a reduction relation casewise, one case for each of the
 clauses beginning with @scheme[-->]. Each of the @scheme[pattern]s
@@ -811,10 +813,14 @@ all non-GUI portions of Redex) and also exported by
 @defform/subs[#:literals (: ->)
               (define-metafunction language-exp
                contract
-               [(name #, @|ttpattern| ...) #, @|tttterm| (side-condition scheme-expression) ...] 
+               [(name #, @|ttpattern| ...) #, @|tttterm| extras ...] 
                ...)
                ([contract (code:line) 
-                          (code:line id : #, @|ttpattern| ... -> #, @|ttpattern|)])]{
+                          (code:line id : #, @|ttpattern| ... -> #, @|ttpattern|)]
+                [extras (side-condition scheme-expression)
+                        (where tl-pat #, @|tttterm|)]
+                [tl-pat identifier (tl-pat-ele ...)]
+                [tl-pat-ele tl-pat (code:line tl-pat ... (code:comment "a literal ellipsis"))])]{
 
 The @scheme[define-metafunction] form builds a function on
 sexpressions according to the pattern and right-hand-side