diff --git a/collects/redex/examples/arithmetic.ss b/collects/redex/examples/arithmetic.ss
index b4911c4735..a9015b32d2 100644
--- a/collects/redex/examples/arithmetic.ss
+++ b/collects/redex/examples/arithmetic.ss
@@ -1,41 +1,41 @@
 #lang scheme
 (require redex)
+
+(define-language lang
+  (e (binop e e)
+     (sqrt e)
+     number)
+  (binop +
+         -
+         *
+         /)
   
-  (define-language lang
-    (e (binop e e)
-       (sqrt e)
-       number)
-    (binop +
-           -
-           *
-           /)
-    
-    (e-ctxt (binop e e-ctxt)
-            (binop e-ctxt e)
-            (sqrt e-ctxt)
-            hole)
-    (v number))
-  
-  (define reductions
-    (reduction-relation
-     lang
-     (c--> (+ number_1 number_2)
-           ,(+ (term number_1) (term number_2))
-           "add")
-     (c--> (- number_1 number_2)
-           ,(- (term number_1) (term number_2))
-           "subtract")
-     (c--> (* number_1 number_2)
-           ,(* (term number_1) (term number_2))
-           "multiply")
-     (c--> (/ number_1 number_2)
-           ,(/ (term number_1) (term number_2))
-           "divide")
-     (c-->(sqrt number_1)
-          ,(sqrt (term number_1))
-          "sqrt")
-     with
-     [(--> (in-hole e-ctxt_1 a) (in-hole e-ctxt_1 b))
-      (c--> a b)]))
-  
-  (traces reductions (term (- (* (sqrt 36) (/ 1 2)) (+ 1 2))))
\ No newline at end of file
+  (e-ctxt (binop e e-ctxt)
+          (binop e-ctxt e)
+          (sqrt e-ctxt)
+          hole)
+  (v number))
+
+(define reductions
+  (reduction-relation
+   lang
+   (c--> (+ number_1 number_2)
+         ,(+ (term number_1) (term number_2))
+         "add")
+   (c--> (- number_1 number_2)
+         ,(- (term number_1) (term number_2))
+         "subtract")
+   (c--> (* number_1 number_2)
+         ,(* (term number_1) (term number_2))
+         "multiply")
+   (c--> (/ number_1 number_2)
+         ,(/ (term number_1) (term number_2))
+         "divide")
+   (c-->(sqrt number_1)
+        ,(sqrt (term number_1))
+        "sqrt")
+   with
+   [(--> (in-hole e-ctxt_1 a) (in-hole e-ctxt_1 b))
+    (c--> a b)]))
+
+(traces reductions (term (- (* (sqrt 36) (/ 1 2)) (+ 1 2))))
diff --git a/collects/redex/examples/beginner.ss b/collects/redex/examples/beginner.ss
index fb521d08c9..06ec094afb 100644
--- a/collects/redex/examples/beginner.ss
+++ b/collects/redex/examples/beginner.ss
@@ -918,6 +918,6 @@ reflects the (broken) spec).
         false)))))
 
 ;; timing test
-;#;
+#;
 (time (run-tests)
       (run-big-test))
\ No newline at end of file
diff --git a/collects/redex/examples/church.ss b/collects/redex/examples/church.ss
index f225ecd895..b3152a11b5 100644
--- a/collects/redex/examples/church.ss
+++ b/collects/redex/examples/church.ss
@@ -47,11 +47,11 @@
       (subst (x_1 e_1 e_3)))]
   [(subst (x_1 e_1 number_1)) number_1])
 
-(traces lang reductions
+(traces reductions
         '(let (plus (lambda (m) 
                       (lambda (n) 
                         (lambda (s)
                           (lambda (z)
                             (app (app m s) (app (app n s) z)))))))
            (let (two (lambda (s) (lambda (z) (app s (app s z)))))
-             (app (app plus two) two))))
\ No newline at end of file
+             (app (app plus two) two))))
diff --git a/collects/redex/examples/combinators.ss b/collects/redex/examples/combinators.ss
index 9d1f4ef1d9..4ccef96047 100644
--- a/collects/redex/examples/combinators.ss
+++ b/collects/redex/examples/combinators.ss
@@ -54,38 +54,11 @@
 (define (make-w b c c*) `(,c ((,c ((,b ,c) ((,c ((,b j) ,c*)) ,c*))) ,c*)))
 (define (make-s b c w) `((,b ((,b (,b ,w)) ,c)) (,b ,b)))
 
-(traces lang
-        relation
+(traces relation
         (list 
          `((,c* abs1) abs2)
          `(((,(make-c 'c*) abs1) abs2) abs3)
          `(((,(make-b 'c) abs1) abs2) abs3)
          `((,(make-w 'b 'c 'c*) abs1) abs2)
          `(((,(make-s 'b 'c 'w) abs1) abs2) abs3))
-        #:multiple #t)
-
-(require (lib "pretty.ss"))
-#;
-(let loop ([t (make-s (make-b (make-c c*))
-                      (make-c c*)
-                      (make-w (make-b (make-c c*))
-                              (make-c c*)
-                              c*))]
-           [i 0])
-  (when (zero? (modulo i 100))
-    (display i)
-    (display " ")
-    (flush-output))
-  (let ([next (apply-reduction-relation ij-relation t)])
-    (if (null? next)
-        (begin (newline) 
-               (pretty-print t))
-        (loop (car next) (+ i 1)))))
-
-#;
-(traces lang ij-relation
-        (make-s (make-b (make-c c*))
-                (make-c c*)
-                (make-w (make-b (make-c c*))
-                        (make-c c*)
-                        c*)))
\ No newline at end of file
+        #:multiple? #t)
diff --git a/collects/redex/examples/compatible-closure.ss b/collects/redex/examples/compatible-closure.ss
index 9187794059..313bcedcd6 100644
--- a/collects/redex/examples/compatible-closure.ss
+++ b/collects/redex/examples/compatible-closure.ss
@@ -14,4 +14,4 @@
 
 (define ->r (compatible-closure r grammar B))
 
-(traces grammar ->r '((f * f) * (t * f)))
+(traces ->r '((f * f) * (t * f)))
diff --git a/collects/redex/examples/letrec.ss b/collects/redex/examples/letrec.ss
index cd638db491..b0970992b3 100644
--- a/collects/redex/examples/letrec.ss
+++ b/collects/redex/examples/letrec.ss
@@ -117,7 +117,7 @@ BUG: letrec & let are not handled properly by substitution
    with
    [(--> a ,(collect (term b))) (==> a b)]))
 
-(define (run e) (traces lang reductions `((store) ,e)))
+(define (run e) (traces reductions `((store) ,e)))
 
 (run '(letrec ((f (lambda (x)
                     (letrec ((y (f 1))) 
diff --git a/collects/redex/examples/omega.ss b/collects/redex/examples/omega.ss
index 927997aed6..30789b4705 100644
--- a/collects/redex/examples/omega.ss
+++ b/collects/redex/examples/omega.ss
@@ -31,6 +31,6 @@
         (in-hole c_1 (subst (variable_x v_arg e_body)))
         βv)))
 
-(traces lang reductions '((lambda (x) (x x)) (lambda (x) (x x))))
-(traces lang reductions '((call/cc call/cc) (call/cc call/cc)))
-(traces lang reductions '((lambda (x) ((call/cc call/cc) x)) (call/cc call/cc)))
+(traces reductions '((lambda (x) (x x)) (lambda (x) (x x))))
+(traces reductions '((call/cc call/cc) (call/cc call/cc)))
+(traces reductions '((lambda (x) ((call/cc call/cc) x)) (call/cc call/cc)))
diff --git a/collects/redex/examples/semaphores.ss b/collects/redex/examples/semaphores.ss
index 5ba1f7718d..14dcbb44a4 100644
--- a/collects/redex/examples/semaphores.ss
+++ b/collects/redex/examples/semaphores.ss
@@ -149,15 +149,13 @@ semaphores make things much more predictable...
            (in-hole c (void))
            e_after ...)))))
 
-(stepper lang
-         reductions
+(stepper reductions
          `((store (y (list)))
            (semas)
            (threads (set! y (cons 1 y))
                     (set! y (cons 2 y)))))
 
-(stepper lang
-         reductions
+(stepper reductions
          `((store (y (list)))
            (semas (x 1))
            (threads (begin (semaphore-wait (semaphore x)) 
diff --git a/collects/redex/examples/subject-reduction.ss b/collects/redex/examples/subject-reduction.ss
index 8d608237cf..108ba8b741 100644
--- a/collects/redex/examples/subject-reduction.ss
+++ b/collects/redex/examples/subject-reduction.ss
@@ -32,7 +32,7 @@
    
    ;; this rules calls subst with the wrong arguments, which is caught by the example below.
    (--> (in-hole c_1 ((lambda (x_format t_1) e_body) v_actual))
-        (in-hole c_1 (subst x_format v_actual e_body))
+        (in-hole c_1 (subst (x_format e_body v_actual)))
         βv)))
 
 (define (type-check term)
@@ -65,6 +65,43 @@
       (and t1
            (equal? (type-check term2) t1)))))
 
+(define-language subst-lang
+  (x variable))
+
+(define-metafunction subst-lang
+  [(subst-n ((x_1 any_1) (x_2 any_2) ... any_3))
+   (subst (x_1 any_1 (subst-n ((x_2 any_2) ... any_3))))]
+  [(subst-n (any_3)) any_3])
+
+(define-metafunction subst-lang
+  ;; 1. x_1 bound, so don't continue in λ body
+  [(subst (x_1 any_1 (λ (x_1 t) any_2)))
+   (λ (x_1 t) any_2)]
+  ;; 2. general purpose capture avoiding case
+  [(subst (x_1 any_1 (λ (x_2 t) any_2)))
+   ,(term-let ([x_new
+                (variable-not-in (term (x_1 any_1 any_2)) 
+                                 (term x_2))])
+              (term 
+               (λ (x_new t) 
+                 (subst (x_1 any_1 (subst-vars ((x_2 x_new) any_2)))))))]
+  ;; 3. replace x_1 with e_1
+  [(subst (x_1 any_1 x_1)) any_1]
+  ;; 4. x_1 and x_2 are different, so don't replace
+  [(subst (x_1 any_1 x_2)) x_2]
+  ;; the last two cases cover all other expression forms
+  [(subst (x_1 any_1 (any_2 ...)))
+   ((subst (x_1 any_1 any_2)) ...)]
+  [(subst (x_1 any_1 any_2)) any_2])
+
+(define-metafunction subst-lang
+  [(subst-vars ((x_1 any_1) x_1)) any_1]
+  [(subst-vars ((x_1 any_1) (any_2 ...))) ((subst-vars ((x_1 any_1) any_2)) ...)]
+  [(subst-vars ((x_1 any_1) any_2)) any_2]
+  [(subst-vars ((x_1 any_1) (x_2 any_2) ... any_3)) 
+   (subst-vars ((x_1 any_1) (subst-vars ((x_2 any_2) ... any_3))))]
+  [(subst-vars (any)) any])
+
 (define (show term)
   (traces reductions term #:pred (pred term)))
 
diff --git a/collects/redex/examples/threads.ss b/collects/redex/examples/threads.ss
index 57b318298d..adcb576e84 100644
--- a/collects/redex/examples/threads.ss
+++ b/collects/redex/examples/threads.ss
@@ -74,13 +74,14 @@
            (set! x (+ x -1))
            (set! x (+ x 1))))
         
+        #:pp
         (lambda (exp)
           (match exp
             [`((store (x ,x)) (threads ,t1 ,t2))
              (format "~a ~a ~a" x (count t1) (count t2))])))
 
 (parameterize ([initial-char-width 16])
-  (stepper threads reductions '((store) (threads 
-                                         (+ 1 1)
-                                         (+ 1 1)
-                                         (+ 1 1)))))
+  (stepper reductions '((store) (threads 
+                                 (+ 1 1)
+                                 (+ 1 1)
+                                 (+ 1 1)))))
diff --git a/collects/redex/pict.ss b/collects/redex/pict.ss
index 0ef7a4ee84..169a02721d 100644
--- a/collects/redex/pict.ss
+++ b/collects/redex/pict.ss
@@ -74,6 +74,9 @@
  lw-column
  lw-column-span)
 
+(provide to-lw
+         (struct-out lw))
+
 (provide/contract
  [just-before (-> (or/c pict? string? symbol?) lw? lw?)]
  [just-after (-> (or/c pict? string? symbol?) lw? lw?)])
diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl
index 6802c9a3d1..7345b9b62e 100644
--- a/collects/redex/redex.scrbl
+++ b/collects/redex/redex.scrbl
@@ -83,9 +83,9 @@ semantics.
 
 This is a reference manual for Redex. See
 @link["http://www.cs.uchicago.edu/~robby/plt-redex/"]{
- @tt{http://www.cs.uchicago.edu/~robby/plt-redex/}
-}
-for a gentler overview.
+@tt{http://www.cs.uchicago.edu/~robby/plt-redex/}} for a gentler
+overview. (See also the @tt{examples} subdirectory in the @tt{redex}
+collection.)
 
 To load Redex use: @defmodule[redex] which provides all of
 the names documented in this library.
@@ -1415,8 +1415,6 @@ it. The thunk may be invoked multiple times when rendering a
 single reduction relation.
 }
 
-@subsection{Pink & LW}
-
 @deftech{Removing the pink background from PLT Redex rendered picts and ps files}
 
 When reduction rules, a metafunction, or a grammar contains
@@ -1501,23 +1499,35 @@ explanation of logical-space):
 }
 
 
-A _lw_ is a struct:
-  (build-lw element posnum posnum posnum posnum)
-with selectors:
->  lw-e :: lw -> element
->  lw-line :: lw -> posnum
->  lw-line-span :: lw -> posnum
->  lw-column :: lw -> posnum
->  lw-column-span :: lw -> posnum
+@subsection{LW}
 
-An _element_ is either:
-  string
-  symbol
-  pict
-  (listof lw)
+@deftogether[[
+@defproc[(build-lw [e (or/c string? symbol? pict? (listof lw?))]
+                   [line exact-positive-integer?]
+                   [line-span exact-positive-integer?]
+                   [column exact-positive-integer?]
+                   [column-span exact-positive-integer?]) 
+         lw?]{}
+@defproc[(lw-e (lw lw?)) (or/c string? symbol? pict? (listof lw?))]{}
+@defproc[(lw-line (lw lw?)) exact-positive-integer?]{}
+@defproc[(lw-line-span (lw lw?)) exact-positive-integer?]{}
+@defproc[(lw-column (lw lw?)) exact-positive-integer?]{}
+@defproc[(lw-column-span (lw lw?)) exact-positive-integer?]{}
+@defproc[(lw? (v any/c)) boolean?]{}
+@defidform[lw]{}]]{
 
-The lw data structure corresponds represents a
-pattern or a Scheme expression that is to be typeset. 
+The lw data structure corresponds represents a pattern or a Scheme
+expression that is to be typeset.  The functions listed above
+construct @scheme[lw] structs, select fields out of them, and
+recognize them. The @scheme[lw] binding can be used with
+@scheme[copy-struct].
+}
+
+@defform[(to-lw arg)]{
+
+This form turns its argument into lw structs that
+contain all of the spacing information just as it would appear
+when being used to typeset.
 
 Each sub-expression corresponds to its own lw, and
 the element indicates what kind of subexpression it is. If
@@ -1595,6 +1605,7 @@ will be lined up underneath each other, but the relative
 positions of "boys" and "fudge" will be determined by the
 natural size of the words as they rendered in the
 appropriate font.
+}
 
 There are two helper functions that make building
 lws easier:
@@ -1614,12 +1625,6 @@ just before or just after that argument. The line-span and
 column-span of the new lw is always zero.
 }
 
-@defform[(to-lw arg)]{
-
-This form turns its argument into lw structs that
-contain all of the spacing information just as it would appear
-when being used to typeset.
-}
 
 @index-section[]
 
diff --git a/collects/redex/reduction-semantics.ss b/collects/redex/reduction-semantics.ss
index b7aa9ee78e..7b681d65c7 100644
--- a/collects/redex/reduction-semantics.ss
+++ b/collects/redex/reduction-semantics.ss
@@ -4,8 +4,7 @@
 (require "private/reduction-semantics.ss"
          "private/matcher.ss"
          "private/term.ss"
-         "private/rg.ss"
-         "private/loc-wrapper.ss")
+         "private/rg.ss")
 
 #;(provide (all-from-out "private/rg.ss"))
 
@@ -40,9 +39,6 @@
          test-predicate
          test-results)
 
-(provide to-lw
-         (struct-out lw))
-
 (provide/contract
  [reduction-relation->rule-names (-> reduction-relation? (listof symbol?))]
  [language-nts (-> compiled-lang? (listof symbol?))]