diff --git a/collects/redex/doc.txt b/collects/redex/doc.txt
index 6fc900e83a..dfab824865 100644
--- a/collects/redex/doc.txt
+++ b/collects/redex/doc.txt
@@ -10,12 +10,6 @@ This collection provides these files:
 
   _pict.ss_: a library for _generating picts and postscript from semantics_
 
-  _subst.ss_: a library for _capture avoiding substitution_.
-
-  _generator.ss_: automatically generates terms from a language
-
-  _schemeunit.ss_: a _plt-redex specific library of schemeunit checks_.
-
 In addition, the examples subcollection contains several
 small languages to demonstrate various different uses of
 this tool:
@@ -1353,141 +1347,6 @@ when being used to typeset.
 
 ======================================================================
 
-The _subst.ss_ library provides these names:
-
-> (subst (match-pattern subst-rhs ...) ...)      SYNTAX
-
-The result of this form is a function that performs capture
-avoiding substitution for a particular (sexp-based)
-language. The function accepts three arguments, a variable,
-a term to substitute and a term to substitute into.
-
-Each of the `match-pattern's specify the forms of
-the language and the `subst-rhs's specify what kind of form
-it is.  Each of the match-patterns are in (lib "match.ss"
-"match")'s pattern language and any variable that they bind
-are available in the <scheme-expression>'s described below.
-
-The language of the subst-rhs follows.
-
-> (variable)
-
-  this means that the rhs for this form is a symbol that
-  should be treated like a variable. Nothing may follow
-  this.
-
-> (constant)
-
-  this means that the rhs for this form is a constant that
-  cannot be renamed. Nothing may follow this.
-
-> (all-vars <scheme-expression>)
-
-This form indicates that this pattern in the language binds
-the variables produced by the
-<scheme-expression>. 
-
-Immediately following this in a subst-rhs must be a (build
-...) form and some number of (subterm ...) or (subterms ...)
-forms.
-
-> (build <scheme-expression>)
-
-This form must come right after an (all-vars ...) form and
-before any (subterm ...) or (subterms ...) forms.
-
-This form tells subst how to reconstruct this term. The
-<scheme-expression> must evaluate to a procedure that
-accepts the (possibly renamed) variables from the all-vars
-clause, and one argument for each of the subterms that
-follow this declaration (with subterms flattened into the
-argument list) in the same order that the subterm or
-subterms declarations are listed.
-
-> (subterm <scheme-expression> <scheme-expression>)
-
-The first <scheme-expression> must be a list of variables
-that is a sub-list of the variables in the all-vars
-expression. The second expression must be an sexp
-corresponding to one of the subexpressions of this
-expression (matched by the match-patten for this clause of
-subst).
-
-> (subterms <scheme-expression> <scheme-expression>)
-
-The first <scheme-expression> must be a list of variables
-that is a sub-list of the variables in the all-vars
-expression. The second expression must be an sexp
-corresponding to one of the subexpressions of this
-expression (matched by the match-patten for this clause of
-subst).
-
-Consider this example of a substitution procedure for the
-lambda calculus:
-
-  (define lc-subst
-    (subst
-     [`(lambda ,vars ,body)
-      (all-vars vars)
-      (build (lambda (vars body) `(lambda ,vars ,body)))
-      (subterm vars body)]
-     [(? symbol?) (variable)]
-     [(? number?) (constant)]
-     [`(,fun ,@(args ...))
-      (all-vars '())
-      (build (lambda (vars fun . args) `(,fun ,@args)))
-      (subterm '() fun)
-      (subterms '() args)]))
-
-The first clause matches lambda expressions with any number
-of arguments and says that there is one subterm, the body of
-the lambda, and that all of the variables are bound in it.
-
-The second clause matches symbols and indicates that they
-are variables.
-
-The third clause matches numbers and indicates that they are
-constants.
-
-The final clause matches function applications. The
-`all-vars' shows that applications introduce no new
-names. The build procedure reconstructs a new application
-form. The subterm declaration says that the function
-position is a subterm with no variables bound in it. The
-subterms declaration says that all of the arguments are
-subterms and that they do not introduce any new terms.
-
-In this program, lc-subst is bound to a function that does
-the substitution. The first argument is the variable to
-substitute for, the second is the term to substitute and the
-final argument is the term to substitute into. For example,
-this call:
-
-  (lc-subst 'q 
-            '(lambda (x) y) 
-            '((lambda (y) (y q)) (lambda (y) y)))
-
-produces this output:
-
-  '((lambda (y@) (y@ (lambda (x) y))) (lambda (y) y))
-
-This library also provides:
-
-> (plt-subst (match-pattern subst-rhs ...) ...)      SYNTAX
-
-This is identical to subst, described above, except that
-the pattern language used is that from (lib "plt-match.ss"), 
-instead of (lib "match.ss").
-
-> subst/proc
-> alpha-rename 
-> free-vars/memoize
-
-Theses functions are the procedure-based interface to
-substitution that subst expands to and uses.
-
-======================================================================
-
 The _iswim.ss_ module in the "examples" sub-collection defines a
 grammar and reductions from "Programming Languages and Lambda Calculi"
 by Felleisen and Flatt.
@@ -1595,85 +1454,3 @@ by Felleisen and Flatt.
 >                 delta*n :: (on? (listof V?) . -> . (union false? V?))
                      delta as a function for any operation.
 
-======================================================================
-
-The _generator.ss_ module provides a tool for generating instances of
-a grammar non-terminal.
-
-> lang->generator-table :: (lang?
-                            (listof number?)
-                            (listof symbol?)
-                            (listof string?)
-                            (listof symbol?)
-                            number?
-                            . -> .
-                            generator-table?)
-
-  Prepares generator information for a particular language,
-  given a set of numbers to use for the `number' keyword, 
-  a set of symbols for `variable' and `variable-except',
-  and a set of string for `string'.
-
-  The fifth argument lists keywords that appear in the grammar but
-  that should be skipped (to limit the generation space). The last
-  argument should be 0, and it is currently ignored.
-
-> for-each-generated :: (generator-table?
-                         (any? number? . -> . any)
-                         generator-table?
-                         symbol?
-                         . -> . any)
-
-  The first argument is a procedure to call with a series of generated
-  grammar instances and each term's size. Instances are generated from
-  smallest to largest; the size of an instance is roughly the size of
-  the proof tree that demonstrates grammar membership.
-
-  The second argument is a generator table created with
-  `lang->generator-table'.
-
-  The third argument is a symbol, the name of a non-terminal for which
-  instances should be generated.
-
-> for-each-generated/size :: (generator-table?
-                              (any? number? . -> . any)
-                              generator-table?
-                              symbol?
-                              . -> . any)
-
-  Like `for-each-generated', except minimum and maximum sizes are
-  provided, and the order of generation is arbitrary (i.e., some
-  larger instances may be generated before smaller instances).
-
-======================================================================
-
-_schemeunit.ss_: This library provides two 'test's and two
-'check's (in Schemeunit terminology):
-
-> (test-reduces reduction-relation term term)
-
-   This check reduces its second argument according to the
-   reductions in the first argument, and compares it to the
-   final argument. It expects the reductions to only produce
-   a single result.
-
-   It uses apply-reduction-rule* to do the reductions (as above).
-
-
-> (check-reduces reduction-relation term term)
-
-  The 'check' version of test-reduces.
-
-> (test-reduces/multiple reduction-relation term (listof term))
-
-   This check reduces its second argument according to the
-   reductions in the first argument, and compares the
-   results to the final argument. The reductions may produce
-   multiple results and those results are expected to be the
-   same as the list in the last argument.
-
-   It uses apply-reduction-relation* to do the reductions (as above).
-
-> (check-reduces/multiple reduction-relation term (listof term))
-
-   The 'check' version of test-reduces/multiple.
diff --git a/collects/redex/generator.ss b/collects/redex/generator.ss
deleted file mode 100644
index 7516a791fe..0000000000
--- a/collects/redex/generator.ss
+++ /dev/null
@@ -1,252 +0,0 @@
-#|
-
-An attempt to automatically test reduction systems;
-this generates terms from a language automatically.
-
-|#
-
-(module generator mzscheme
-  (require "private/matcher.ss")
-
-  (provide lang->generator-table
-           for-each-generated
-           for-each-generated/size)
-  
-  (define (lang->generator-table lang
-				 nums
-				 vars
-				 strs
-				 skip-kws
-				 cache-limit)
-
-    ;; -------------------- Cache implementation --------------------
-    ;; Cache is currently disabled. It's not clear that it's useful.
-    (define (cache-small gen) gen)
-    
-    ;; -------------------- Build table --------------------
-    ;; The `gens' table maps non-terminal symbols to
-    ;; generator functions. A generator function conumes:
-    ;;   * the min acceptable size of a generated element
-    ;;   * the max acceptable size of a generated element
-    ;;   * a sucess continuation proc that accepts
-    ;;        - the generated value
-    ;;        - the value's size
-    ;;        - a generator proc that produces the next value;
-    ;;          this proc expects to be given the same min, max,
-    ;;          and fail continuation proc as before
-    ;;   * a failure continuation thunk
-    ;;
-    (let ([nts (compiled-lang-lang lang)]
-          [nt-map (make-hash-table)])
-      ;; nt-map tells us which symbols are non-terminals; it also 
-      ;; provides conservative min-size and max-size thunks that are
-      ;; refined as table generation proceeds
-      (for-each (lambda (nt) (hash-table-put! nt-map (nt-name nt) 
-                                              (cons (lambda () 1)
-                                                    (lambda () +inf.0))))
-                nts)
-      ;; gens is the main hash table
-      (let ([gens (make-hash-table)]
-            [atomic-alts (lambda (l size)
-                           (values
-                            (lambda (min-size max-size result-k fail-k)
-			      (let loop ([l l][result-k result-k][max-size max-size][fail-k fail-k])
-				(if (<= min-size size max-size)
-                                    (if (null? l)
-                                        (fail-k)
-                                        (result-k (car l)
-						  size
-						  (lambda (s xs result-k fail-k)
-						    (loop (cdr l) result-k xs fail-k))))
-				    (fail-k))))
-                            (lambda () size)
-                            (lambda () size)))]
-            [to-do nts])
-        (letrec ([make-gen/get-size
-                  (lambda (p)
-                    (cond
-                      [(hash-table-get nt-map p (lambda () #f))
-                       => (lambda (get-sizes)
-                            (values
-                             (lambda (min-size max-size result-k fail-k)
-                               ((hash-table-get gens p) min-size max-size result-k fail-k))
-                             (car get-sizes)
-                             (cdr get-sizes)))]
-                      [(eq? 'number p) (atomic-alts nums 1)]
-                      [(eq? 'string p) (atomic-alts strs 1)]
-                      [(eq? 'any p) (atomic-alts (append nums strs vars) 1)]
-                      [(or (eq? 'variable p)
-                           (and (pair? p)
-                                (eq? (car p) 'variable-except)))
-                       (atomic-alts vars 1)]
-                      [(symbol? p) ; not a non-terminal, because we checked above
-		       (if (memq p skip-kws)
-			   (values
-			    (lambda (min-size max-size result-k fail-k)
-			      (fail-k))
-			    (lambda () +inf.0)
-			    (lambda () -1))
-			   (atomic-alts (list p) 0))]
-                      [(null? p) (atomic-alts (list null) 0)]
-                      [(and (pair? p)
-                            (or (not (pair? (cdr p)))
-                                (not (eq? '... (cadr p)))))
-                       (make-pair-gen/get-size p cons)]
-                      [(and (pair? p) (pair? (cdr p)) (eq? '... (cadr p)))
-		       (let-values ([(just-rest just-rest-min-size just-rest-max-size)
-				     (make-gen/get-size (cddr p))]
-				    [(both both-min-size both-max-size)
-				     (make-pair-gen/get-size (cons (kleene+ (car p)) (cddr p)) append)])
-			 (values
-			  (lambda (min-size max-size result-k fail-k)
-			    (let loop ([both both][result-k result-k][max-size max-size][fail-k fail-k])
-			      (both min-size max-size
-				    (lambda (v size next-both)
-				      (result-k v size
-						(lambda (ns xs result-k fail-k)
-						  (loop next-both result-k xs fail-k))))
-				    (lambda ()
-				      (just-rest min-size max-size result-k fail-k)))))
-			  just-rest-min-size
-			  (lambda () +inf.0)))]
-                      [else
-                       (error 'make-gen "unrecognized pattern: ~e" p)]))]
-                 [make-pair-gen/get-size
-                  (lambda (p combiner)
-                    (let*-values ([(first first-min-size first-max-size) 
-                                   (make-gen/get-size (car p))]
-                                  [(rest rest-min-size rest-max-size) 
-                                   (make-gen/get-size (cdr p))]
-                                  [(this-min-size) (let ([v #f])
-						     (lambda ()
-						       (unless v
-							 (set! v (+ (first-min-size)
-								    (rest-min-size))))
-						       v))]
-                                  [(this-max-size) (let ([v #f])
-						     (lambda ()
-						       (unless v
-							 (set! v (+ (first-max-size)
-								    (rest-max-size))))
-						       v))])
-                      (values
-                       (cache-small
-                        (lambda (min-size max-size result-k fail-k)
-			  (if (min-size . > . (this-max-size))
-			      (fail-k)
-			      (let rloop ([rest rest][result-k result-k][max-size max-size][fail-k fail-k][failed-size +inf.0])
-				(if (max-size . < . (this-min-size))
-				    (fail-k)
-				    (rest
-				     (max 0 (- min-size (first-max-size)))
-				     (min (sub1 failed-size) (- max-size (first-min-size)))
-				     (lambda (rest rest-size next-rest)
-				       (if (rest-size . >= . failed-size)
-					   (rloop next-rest result-k max-size fail-k failed-size)
-					   (let floop ([first first]
-						       [result-k result-k]
-						       [max-size max-size]
-						       [fail-k fail-k] 
-						       [first-fail-k (lambda ()
-								       (rloop next-rest result-k max-size fail-k rest-size))])
-					     (first (max 0 (- min-size rest-size))
-						    (- max-size rest-size)
-						    (lambda (first first-size next-first)
-						      (result-k 
-						       (combiner first rest)
-						       (+ first-size rest-size)
-						       (lambda (ns xs result-k fail-k)
-							 (floop next-first result-k xs fail-k
-								(lambda ()
-								  (rloop next-rest result-k xs fail-k failed-size))))))
-						    first-fail-k))))
-				     fail-k))))))
-                       this-min-size
-                       this-max-size)))]
-                 [kleene+ (lambda (p)
-			    (let ([n (gensym)])
-			      (hash-table-put! nt-map n (cons (lambda () 1)
-							      (lambda () +inf.0)))
-			      (set! to-do (cons (make-nt 
-						 n 
-						 (list (make-rhs (cons p '()))
-						       (make-rhs (cons p n))))
-						to-do))
-			      n))])
-          (let to-do-loop ([nts (reverse to-do)])
-            (set! to-do null)
-            (for-each (lambda (nt)
-                        (hash-table-put!
-                         gens
-                         (nt-name nt)
-                         (let* ([gens+sizes
-                                 (map (lambda (rhs)
-                                        (let-values ([(gen get-min-size get-max-size)
-                                                      (make-gen/get-size 
-                                                       (rhs-pattern rhs))])
-					  (cons gen (cons get-min-size get-max-size))))
-                                      (nt-rhs nt))]
-                                [get-min-size
-                                 (let ([get-min-sizes (map cadr gens+sizes)])
-                                   (let ([v #f])
-                                     (lambda ()
-                                       (unless v
-                                         (set! v (add1
-						  (apply min (map (lambda (gs) (gs))
-								  get-min-sizes)))))
-				       v)))]
-                                [get-max-size
-                                 (let ([get-max-sizes (map cddr gens+sizes)])
-                                   (let ([v #f])
-                                     (lambda ()
-                                       (unless v
-                                         (set! v (add1
-						  (apply max (map (lambda (gs) (gs))
-								  get-max-sizes)))))
-                                       v)))])
-                           (hash-table-put! nt-map (nt-name nt)
-                                            (cons get-min-size get-max-size))
-                           (cache-small
-                            (lambda (min-size max-size result-k fail-k)
-			      (if (min-size . > . (get-max-size))
-                                  (fail-k)
-                                  (let loop ([l (map car gens+sizes)][result-k result-k][max-size max-size][fail-k fail-k])
-				    (if (max-size . < . (get-min-size))
-					(fail-k)
-					(if (null? l)
-					    (fail-k)
-					    (let iloop ([alt-next (car l)]
-							[result-k result-k]
-							[max-size max-size]
-							[fail-k fail-k])
-					      (alt-next
-					       (max 0 (sub1 min-size))
-					       (sub1 max-size)
-					       (lambda (alt a-size alt-next)
-						 (result-k
-						  alt
-						  (add1 a-size)
-						  (lambda (ns xs result-k fail-k)
-						    (iloop alt-next result-k xs fail-k))))
-					       (lambda ()
-						 (loop (cdr l) result-k max-size fail-k)))))))))))))
-                      nts)
-            (unless (null? to-do)
-              (to-do-loop to-do))))
-	gens)))
-  
-  (define (for-each-generated/size proc gens min-size max-size nonterm)
-    (let ([gen (hash-table-get gens nonterm)])
-      (let loop ([gen gen])
-        (gen
-         min-size
-         max-size
-         (lambda (val z1 gen-next)
-           (proc val z1)
-           (loop gen-next))
-         void))))
-  
-  (define (for-each-generated proc gens nonterm)
-    (let loop ([i 0])
-      (for-each-generated/size proc gens i i nonterm)
-      (loop (add1 i)))))
diff --git a/collects/redex/main.ss b/collects/redex/main.ss
new file mode 100644
index 0000000000..1bdf2e876c
--- /dev/null
+++ b/collects/redex/main.ss
@@ -0,0 +1,7 @@
+#lang scheme/base
+(require "reduction-semantics.ss"
+         "gui.ss"
+         "pict.ss")
+(provide (all-from-out "reduction-semantics.ss"
+                       "gui.ss" 
+                       "pict.ss"))
\ No newline at end of file
diff --git a/collects/redex/schemeunit.ss b/collects/redex/schemeunit.ss
deleted file mode 100644
index 402b095f43..0000000000
--- a/collects/redex/schemeunit.ss
+++ /dev/null
@@ -1,43 +0,0 @@
-#lang scheme
-
-(require (planet "test.ss" ("schematics" "schemeunit.plt" 2))
-         (except-in "reduction-semantics.ss" check))
-
-(provide test-reduces 
-         check-reduces 
-         test-reduces/multiple
-         check-reduces/multiple)
-
-(define-shortcut (test-reduces reds from to) (check-reduces reds from to))
-
-(define-check (check-reduces reds from to)
-  (let ([all (apply-reduction-relation* reds from)])
-    (cond
-      [(null? (cdr all))
-       (unless (equal? (car all) to)
-         (with-check-info
-          (('expected to)
-           ('actual (car all)))
-          (fail-check)))]
-      [else
-       (with-check-info
-        (('multiple-results all))
-        (fail-check))])))
-
-(define-shortcut (test-reduces/multiple reds from to) (check-reduces/multiple reds from to))
-
-(define-check (check-reduces/multiple reds from to)
-  (let ([all (apply-reduction-relation* reds from)])
-    (unless (set-equal? all to)
-      (with-check-info
-       (('expecteds to)
-        ('actuals all))
-       (fail-check)))))
-
-(define (set-equal? s1 s2)
-  (define (subset? a b)
-    (let ([ht (make-hash)])
-      (for-each (λ (x) (hash-set! ht x #t)) a)
-      (andmap (λ (x) (hash-ref ht x #f)) b)))
-  (and (subset? s1 s2)
-       (subset? s2 s1)))
\ No newline at end of file
diff --git a/collects/redex/subst.ss b/collects/redex/subst.ss
deleted file mode 100644
index 080224c857..0000000000
--- a/collects/redex/subst.ss
+++ /dev/null
@@ -1,292 +0,0 @@
-(module subst mzscheme
-  (require (lib "match.ss")
-           (prefix plt: (lib "plt-match.ss"))
-           (lib "list.ss"))
-  
-  (provide plt-subst subst
-           all-vars variable subterm subterms constant build
-           subst/proc alpha-rename free-vars/memoize)
-  
-  (define-syntax (all-vars stx) (raise-syntax-error 'subst "all-vars out of context" stx))
-  (define-syntax (variable stx) (raise-syntax-error 'subst "variable out of context" stx))
-  (define-syntax (subterm stx) (raise-syntax-error 'subst "subterm out of context" stx))
-  (define-syntax (subterms stx) (raise-syntax-error 'subst "subterms out of context" stx))
-  (define-syntax (constant stx) (raise-syntax-error 'subst "constant out of context" stx))
-  (define-syntax (build stx) (raise-syntax-error 'subst "build out of context" stx))
-  
-  (define-syntax (make-subst stx)
-    (syntax-case stx ()
-      [(_ subst match)
-       (syntax
-        (define-syntax (subst stx)
-          (syntax-case stx ()
-            [(_ (pat rhs (... ...)) (... ...))
-             (with-syntax ([term/arg #'term/arg]
-                           [constant/arg #'constant/arg]
-                           [variable/arg #'variable/arg]
-                           [combine/arg #'combine/arg]
-                           [sub-piece/arg #'subpiece/arg])
-               (define (handle-rhs rhs-stx)
-                 (syntax-case rhs-stx (all-vars build subterm subterms variable constant)
-                   [((all-vars all-vars-exp) (build build-exp) sub-pieces (... ...))
-                    (with-syntax ([(sub-pieces (... ...))
-                                   (map (lambda (subterm-stx)
-                                          (syntax-case subterm-stx (subterm subterms)
-                                            [(subterm vars body) (syntax (list (sub-piece/arg vars body)))]
-                                            [(subterms vars terms) 
-                                             (syntax 
-                                              (let ([terms-var terms])
-                                                (unless (list? terms-var)
-                                                  (error 'subst
-                                                         "expected a list of terms for `subterms' subclause, got: ~e"
-                                                         terms-var))
-                                                (map (lambda (x) (sub-piece/arg vars x))
-                                                     terms-var)))]
-                                            [else (raise-syntax-error 
-                                                   'subst 
-                                                   "unknown all-vars subterm"
-                                                   stx
-                                                   subterm-stx)]))
-                                        (syntax->list (syntax (sub-pieces (... ...)))))])
-                      (syntax
-                       (apply combine/arg
-                              build-exp
-                              all-vars-exp
-                              (append sub-pieces (... ...)))))]
-                   [((all-vars) sub-pieces (... ...))
-                    (raise-syntax-error 'subst "expected all-vars must have an argument" stx rhs-stx)]
-                   [((all-vars all-vars-exp) not-build-clause anything (... ...))
-                    (raise-syntax-error 'subst "expected build clause" (syntax not-build-clause))]
-                   [((all-vars all-vars-exp))
-                    (raise-syntax-error 'subst "missing build clause" (syntax (all-vars all-vars-exp)))]
-                   [((constant)) 
-                    (syntax (constant/arg term/arg))]
-                   [((variable))
-                    (syntax (variable/arg (lambda (x) x) term/arg))]
-                   [(unk unk-more (... ...))
-                    (raise-syntax-error 'subst "unknown clause" (syntax unk))]))
-               (with-syntax ([(expanded-rhs (... ...))
-                              (map handle-rhs (syntax->list (syntax ((rhs (... ...)) (... ...)))))])
-                 (syntax
-                  (let ([separate
-                         (lambda (term/arg constant/arg variable/arg combine/arg sub-piece/arg)
-                           (match term/arg
-                             [pat expanded-rhs] (... ...)
-                             [else (error 'subst "no matching clauses for ~s\n" term/arg)]))])
-                    (lambda (var val exp)
-                      (subst/proc var val exp separate))))))])))]))
-  
-  (make-subst subst match)
-  (make-subst plt-subst plt:match)
-  
-  (define (subst/proc var val exp separate)
-    (let* ([free-vars-cache (make-hash-table 'equal)]
-           [fv-val (free-vars/memoize free-vars-cache val separate)])
-      (let loop ([exp exp])
-        (let ([fv-exp (free-vars/memoize free-vars-cache exp separate)]
-              [handle-constant
-               (lambda (x) x)]
-              [handle-variable
-               (lambda (rebuild var-name)
-                 (if (equal? var-name var)
-                     val
-                     (rebuild var-name)))]
-              [handle-complex
-               (lambda (maker vars . subpieces)
-                 (cond
-                   [(ormap (lambda (var) (memq var fv-val)) vars)
-                    =>
-                    (lambda (to-be-renamed-l)
-                      (let ([to-be-renamed (car to-be-renamed-l)])
-                        (loop
-                         (alpha-rename
-                          to-be-renamed
-                          (pick-new-name to-be-renamed (cons to-be-renamed fv-val))
-                          exp
-                          separate))))]
-                   [else
-                    (apply maker 
-                           vars
-                           (map (lambda (subpiece)
-                                  (let ([sub-term-binders (subpiece-binders subpiece)]
-                                        [sub-term (subpiece-term subpiece)])
-                                    (if (memq var sub-term-binders)
-                                        sub-term
-                                        (loop sub-term))))
-                                subpieces))]))])
-          (if (member var fv-exp)
-              (separate
-               exp
-               handle-constant
-               handle-variable
-               handle-complex
-               make-subpiece)
-              exp)))))
-  
-  (define-struct subpiece (binders term) (make-inspector))
-  
-  ;; alpha-rename : symbol symbol term separate -> term
-  ;; renames the occurrences of to-be-renamed that are 
-  ;; bound in the "first level" of exp.
-  (define (alpha-rename to-be-renamed new-name exp separate)
-    (define (first exp)
-      (separate exp
-                first-handle-constant
-                first-handle-variable
-                first-handle-complex
-                first-handle-complex-subpiece))
-    (define (first-handle-constant x) x)
-    (define (first-handle-variable rebuild var) (rebuild var))
-    (define (first-handle-complex maker vars . subpieces)
-      (let ([replaced-vars
-             (map (lambda (x) (if (eq? x to-be-renamed) new-name x))
-                  vars)])
-        (apply maker replaced-vars subpieces)))
-    (define (first-handle-complex-subpiece binders subterm)
-      (if (memq to-be-renamed binders)
-          (beyond-first subterm)
-          subterm))
-    
-    (define (beyond-first exp)
-      (define (handle-constant x) x)
-      (define (handle-variable rebuild var)
-        (if (eq? var to-be-renamed)
-            (rebuild new-name)
-            (rebuild var)))
-      (define (handle-complex maker vars . subpieces)
-        (apply maker vars subpieces))
-      (define (handle-complex-subpiece binders subterm)
-        (if (memq to-be-renamed binders)
-            subterm
-            (beyond-first subterm)))
-      (separate
-       exp
-       handle-constant
-       handle-variable
-       handle-complex
-       handle-complex-subpiece))
-    
-    (first exp))
-  
-  ;; free-vars/memoize : hash-table[sexp -o> (listof symbols)] sexp separate -> (listof symbols)
-  ;; doesn't cache against separate -- if it changes, a new hash-table must be passed in,
-  ;; or the caching will be wrong
-  (define (free-vars/memoize cache exp separate)
-    (hash-table-get
-     cache
-     exp
-     (lambda ()
-       (let ([res (free-vars/compute cache exp separate)])
-         (hash-table-put! cache exp res)
-         res))))
-  
-  ;; free-vars/memoize : hash-table[sexp -o> (listof symbols)] sexp separate -> (listof symbols)
-  (define (free-vars/compute cache exp separate)
-    (let ([handle-constant (lambda (x) '())]
-          [handle-variable (lambda (rebuild var) (list var))]
-          [handle-complex
-           (lambda (maker vars . subpieces)
-             (apply append subpieces))]
-          [handle-complex-subpiece
-           (lambda (binders subterm)
-             (foldl remove-all
-                    (free-vars/memoize cache subterm separate)
-                    binders))])
-      (separate
-       exp
-       handle-constant
-       handle-variable
-       handle-complex
-       handle-complex-subpiece)))
-  
-  (define (remove-all var lst)
-    (let loop ([lst lst]
-               [ans '()])
-      (cond
-        [(null? lst) ans]
-        [else (if (eq? (car lst) var)
-                  (loop (cdr lst) ans)
-                  (loop (cdr lst) (cons (car lst) ans)))])))
-  
-  (define (lc-direct-subst var val exp)
-    (let ([fv-exp (lc-direct-free-vars exp)])
-      (if (memq var fv-exp)
-          (match exp
-            [`(lambda ,vars ,body)
-             (if (memq var vars)
-                 exp
-                 (let* ([fv-val (lc-direct-free-vars val)]
-                        [vars1 (map (lambda (var) (pick-new-name var fv-val)) vars)])
-                   `(lambda ,vars1 ,(lc-direct-subst
-                                     var 
-                                     val
-                                     (lc-direct-subst/l vars 
-                                                        vars1
-                                                        body)))))]
-            [`(let (,l-var ,exp) ,body)
-             (if (eq? l-var var)
-                 `(let (,l-var ,(lc-direct-subst var val exp)) ,body)
-                 (let* ([fv-val (lc-direct-free-vars val)]
-                        [l-var1 (pick-new-name l-var fv-val)])
-                   `(let (,l-var1 ,(lc-direct-subst var val exp))
-                      ,(lc-direct-subst
-                        var 
-                        val
-                        (lc-direct-subst
-                         l-var 
-                         l-var1
-                         body)))))]
-            [(? number?) exp]
-            [(and var1 (? symbol?))
-             (if (eq? var1 var)
-                 val
-                 var1)]
-            [`(,@(args ...))
-             `(,@(map (lambda (arg) (lc-direct-subst var val arg)) args))])
-          exp)))
-  
-  ;; lc-direct-subst/l : (listof symbol) (listof symbol) (listof symbol) sexp -> exp
-  ;; substitutes each of vars with vals in exp
-  ;; [assume vals don't contain any vars]
-  (define (lc-direct-subst/l vars vals exp)
-    (foldr (lambda (var val exp) (lc-direct-subst var val exp))
-           exp
-           vars
-           vals))
-  
-  ;; lc-direct-free-vars : sexp -> (listof symbol)
-  ;; returns the free variables in exp
-  (define (lc-direct-free-vars exp)
-    (let ([ht (make-hash-table)])
-      (let loop ([exp exp]
-                 [binding-vars null])
-        (match exp
-          [(? symbol?) 
-           (unless (memq exp binding-vars)
-             (hash-table-put! ht exp #t))]
-          [(? number?)
-           (void)]
-          [`(lambda ,vars ,body)
-           (loop body (append vars binding-vars))]
-          [`(let (,var ,exp) ,body)
-           (loop exp binding-vars)
-           (loop body (cons var binding-vars))]
-          [`(,@(args ...))
-           (for-each (lambda (arg) (loop arg binding-vars)) args)]))
-      (hash-table-map ht (lambda (x y) x))))
-  
-  ;; pick-new-name : symbol (listof symbol) -> symbol
-  ;; returns a primed version of `var' that does
-  ;; not occur in vars (possibly with no primes)
-  (define (pick-new-name var vars)
-    (if (member var vars)
-        (pick-new-name (prime var) vars)
-        var))
-  
-  ;; prime : symbol -> symbol
-  ;; adds an @ at the end of the symbol
-  (define (prime var)
-    (string->symbol
-     (string-append
-      (symbol->string var)
-      "@"))))
\ No newline at end of file