diff --git a/collects/redex/private/bitmap-test-util.ss b/collects/redex/private/bitmap-test-util.ss
index 1a3b8ab32a..cf2dcada8d 100644
--- a/collects/redex/private/bitmap-test-util.ss
+++ b/collects/redex/private/bitmap-test-util.ss
@@ -1,171 +1,161 @@
-(module bitmap-test-util mzscheme
-  (require (lib "mred.ss" "mred")
-           (lib "mrpict.ss" "texpict")
-           (lib "framework.ss" "framework")
-           (lib "class.ss")
-           "../pict.ss"
-           "../reduction-semantics.ss")
-  
-  (provide test done)
-  
-  (define-struct failed-test (panel))
-  
-  (define show-diffs?-env "PLT_REDEX_TEST_NOSHOW_DIFFS")
-  (define show-diffs? (not (getenv show-diffs?-env)))
-  
-  (define tests 0)
-  (define failed '())
-  (define (done)
-    (printf "~a tests" tests)
-    (if (null? failed)
-        (printf ", all passed\n")
-        (printf ", ~a failed\n" (length failed))))
-  
-  (define-syntax (test stx)
-    (syntax-case stx ()
-      [(_ test-exp bitmap-filename)
-       #`(test/proc
-          #,(syntax-line stx)
-          test-exp
-          bitmap-filename)]))
-  
-  (define (test/proc line-number pict raw-bitmap-filename)
-    (set! tests (+ tests 1))
-    (let* ([bitmap-filename 
-            (build-path "bmps" 
-                        (case (system-type)
-                          [(unix) (string-append "unix-" raw-bitmap-filename)]
-                          [else raw-bitmap-filename]))]
-           [old-bitmap (if (file-exists? bitmap-filename)
-                           (make-object bitmap% bitmap-filename)
-                           (let* ([bm (make-object bitmap% 100 20)]
-                                  [bdc (make-object bitmap-dc% bm)])
-                             (send bdc clear)
-                             (send bdc draw-text "does not exist" 0 0)
-                             (send bdc set-bitmap #f)
-                             bm))]
-           [new-bitmap (make-object bitmap% 
-                         (inexact->exact (pict-width pict)) 
-                         (inexact->exact (pict-height pict)))]
-           [bdc (make-object bitmap-dc% new-bitmap)])
-      (send bdc clear)
-      (draw-pict pict bdc 0 0)
-      (send bdc set-bitmap #f)
-      (let ([diff-bitmap (compute-diffs old-bitmap new-bitmap)])
-        (when diff-bitmap
-          (if show-diffs?
-              (let ([failed-panel (make-failed-panel line-number bitmap-filename old-bitmap new-bitmap diff-bitmap)])
-                (set! failed (append failed (list (make-failed-test failed-panel)))))
-              (set! failed (append failed (list #f))))))))
-  
-  (define (compute-diffs old-bitmap new-bitmap)
-    (let* ([w (max (send old-bitmap get-width)
-                   (send new-bitmap get-width))]
-           [h (max (send old-bitmap get-height)
-                   (send new-bitmap get-height))]
-           [diff-bitmap (make-object bitmap% w h)]
-           [new (make-object bitmap-dc% new-bitmap)]
-           [old (make-object bitmap-dc% old-bitmap)]
-           [diff (make-object bitmap-dc% diff-bitmap)]
-           [new-c (make-object color%)]
-           [old-c (make-object color%)]
-           [any-different? #f])
-      (let loop ([x 0])
-        (unless (= x w)
-          (let loop ([y 0])
-            (unless (= y h)
-              (cond
-                [(and (<= x (send new-bitmap get-width))
-                      (<= y (send new-bitmap get-height))
-                      (<= x (send old-bitmap get-width))
-                      (<= y (send old-bitmap get-height)))
-                 (send new get-pixel x y new-c)
-                 (send old get-pixel x y old-c)
-                 (cond
-                   [(and (= (send new-c red) (send old-c red))
-                         (= (send new-c green) (send old-c green))
-                         (= (send new-c blue) (send old-c blue)))
-                    (send diff set-pixel x y new-c)]
-                   [else
-                    (set! any-different? #t)
-                    (send new-c set 255 0 0)
-                    (send diff set-pixel x y new-c)])]
-                [else 
-                 (set! any-different? #t)
-                 (send new-c set 255 0 0)
-                 (send diff set-pixel x y new-c)])
-              (loop (+ y 1))))
-          (loop (+ x 1))))
-      (send diff set-bitmap #f)
-      (send old set-bitmap #f)
-      (send new set-bitmap #f)
-      (and any-different? diff-bitmap)))
-  
-  (define test-result-single-panel #f)
-  (define (get-test-result-single-panel)
-    (cond
-      [test-result-single-panel
-       test-result-single-panel]
-      [else
-       (let ()
-         (define f (new frame% [label "bitmap-test.ss failures"]))
-         (define lined (new vertical-panel% [parent f] [style '(border)]))
-         (define sp (new panel:single% [parent lined]))
-         (define current-index 0)
-         (define hp (new horizontal-panel% [parent f]))
-         (define prev 
-           (new button% 
-                [label "Prev"] 
-                [parent hp]
-                [callback
-                 (λ (x y)
-                   (set! current-index (modulo (- current-index 1) (length failed)))
-                   (update-gui))]))
-         (define next (new button% 
-                           [label "Next"] 
-                           [parent hp]
-                           [callback
-                            (λ (x y)
-                              (set! current-index (modulo (+ current-index 1) (length failed)))
-                              (update-gui))]))
-         (define (update-gui) 
-           (send sp active-child (failed-test-panel (list-ref failed current-index))))
-         (set! test-result-single-panel sp)
-         (send f show #t)
-         sp)]))
-  
-  (define (make-failed-panel line-number filename old-bitmap new-bitmap diff-bitmap)
-    (define f (new vertical-panel% [parent (get-test-result-single-panel)]))
-    (define msg (new message% [label (format "line ~a" line-number)] [parent f]))
-    (define hp (new horizontal-panel% [parent f]))
-    (define vp1 (new vertical-panel% [parent hp]))
-    (define vp2 (new vertical-panel% [parent hp]))
-    (define chk (new check-box% 
-                     [label "Show diff"]
-                     [parent f]
-                     [callback
-                      (λ (_1 _2)
-                        (cond
-                          [(send chk get-value)
-                           (send chk set-label "Hide diff")
-                           (send right-hand set-label diff-bitmap)]
-                          [else
-                           (send chk set-label "Show diff")
-                           (send right-hand set-label new-bitmap)]))]))
-    (define btn (new button%
-                     [parent f]
-                     [label "Save"]
-                     [callback
-                      (λ (x y)
-                        (send new-bitmap save-file filename 'png))]))
-    (define left-label (new message% [parent vp1] [label "Old"]))
-    (define left-hand (new message%
-                           [parent vp1]
-                           [label diff-bitmap]))
-    (define right-label (new message% [parent vp2] [label "New"]))
-    (define right-hand (new message%
-                            [parent vp2]
-                            [label diff-bitmap]))
-    (send left-hand set-label old-bitmap)
-    (send right-hand set-label new-bitmap)
-    f))
+#lang scheme/gui
+(require framework
+         slideshow
+         "../pict.ss"
+         "../reduction-semantics.ss"
+         "config.ss")
+
+(provide test done)
+
+(define tests 0)
+(define failed '())
+(define (done)
+  (printf "~a tests" tests)
+  (if (null? failed)
+      (printf ", all passed\n")
+      (printf ", ~a failed\n" (length failed))))
+
+(define-syntax (test stx)
+  (syntax-case stx ()
+    [(_ test-exp bitmap-filename)
+     #`(test/proc
+        #,(syntax-line stx)
+        test-exp
+        bitmap-filename)]))
+
+(define (test/proc line-number pict raw-bitmap-filename)
+  (set! tests (+ tests 1))
+  (let* ([bitmap-filename 
+          (build-path (format "bmps-~a" (system-type))
+                      (case (system-type)
+                        [(unix) (string-append "unix-" raw-bitmap-filename)]
+                        [else raw-bitmap-filename]))]
+         [old-bitmap (if (file-exists? bitmap-filename)
+                         (make-object bitmap% bitmap-filename)
+                         (let* ([bm (make-object bitmap% 100 20)]
+                                [bdc (make-object bitmap-dc% bm)])
+                           (send bdc clear)
+                           (send bdc draw-text "does not exist" 0 0)
+                           (send bdc set-bitmap #f)
+                           bm))]
+         [new-bitmap (make-object bitmap% 
+                       (inexact->exact (pict-width pict)) 
+                       (inexact->exact (pict-height pict)))]
+         [bdc (make-object bitmap-dc% new-bitmap)])
+    (send bdc clear)
+    (draw-pict pict bdc 0 0)
+    (send bdc set-bitmap #f)
+    (let ([diff-bitmap (compute-diffs old-bitmap new-bitmap)])
+      (when diff-bitmap
+        (let ([failed-panel (make-failed-panel line-number bitmap-filename old-bitmap new-bitmap diff-bitmap)])
+          (set! failed (append failed (list failed-panel))))))))
+
+(define (compute-diffs old-bitmap new-bitmap)
+  (let* ([w (max (send old-bitmap get-width)
+                 (send new-bitmap get-width))]
+         [h (max (send old-bitmap get-height)
+                 (send new-bitmap get-height))]
+         [diff-bitmap (make-object bitmap% w h)]
+         [new (make-object bitmap-dc% new-bitmap)]
+         [old (make-object bitmap-dc% old-bitmap)]
+         [diff (make-object bitmap-dc% diff-bitmap)]
+         [new-c (make-object color%)]
+         [old-c (make-object color%)]
+         [any-different? #f])
+    (let loop ([x 0])
+      (unless (= x w)
+        (let loop ([y 0])
+          (unless (= y h)
+            (cond
+              [(and (<= x (send new-bitmap get-width))
+                    (<= y (send new-bitmap get-height))
+                    (<= x (send old-bitmap get-width))
+                    (<= y (send old-bitmap get-height)))
+               (send new get-pixel x y new-c)
+               (send old get-pixel x y old-c)
+               (cond
+                 [(and (= (send new-c red) (send old-c red))
+                       (= (send new-c green) (send old-c green))
+                       (= (send new-c blue) (send old-c blue)))
+                  (send diff set-pixel x y new-c)]
+                 [else
+                  (set! any-different? #t)
+                  (send new-c set 255 0 0)
+                  (send diff set-pixel x y new-c)])]
+              [else 
+               (set! any-different? #t)
+               (send new-c set 255 0 0)
+               (send diff set-pixel x y new-c)])
+            (loop (+ y 1))))
+        (loop (+ x 1))))
+    (send diff set-bitmap #f)
+    (send old set-bitmap #f)
+    (send new set-bitmap #f)
+    (and any-different? diff-bitmap)))
+
+(define test-result-single-panel #f)
+(define (get-test-result-single-panel)
+  (cond
+    [test-result-single-panel
+     test-result-single-panel]
+    [else
+     (let ()
+       (define f (new frame% [label "bitmap-test.ss failures"]))
+       (define lined (new vertical-panel% [parent f] [style '(border)]))
+       (define sp (new panel:single% [parent lined]))
+       (define current-index 0)
+       (define hp (new horizontal-panel% [parent f]))
+       (define prev 
+         (new button% 
+              [label "Prev"] 
+              [parent hp]
+              [callback
+               (λ (x y)
+                 (set! current-index (modulo (- current-index 1) (length failed)))
+                 (update-gui))]))
+       (define next (new button% 
+                         [label "Next"] 
+                         [parent hp]
+                         [callback
+                          (λ (x y)
+                            (set! current-index (modulo (+ current-index 1) (length failed)))
+                            (update-gui))]))
+       (define (update-gui) 
+         (send sp active-child (list-ref failed current-index)))
+       (set! test-result-single-panel sp)
+       (when (get-show-bitmaps?) (send f show #t))
+       sp)]))
+
+(define (make-failed-panel line-number filename old-bitmap new-bitmap diff-bitmap)
+  (define f (new vertical-panel% [parent (get-test-result-single-panel)]))
+  (define msg (new message% [label (format "line ~a" line-number)] [parent f]))
+  (define hp (new horizontal-panel% [parent f]))
+  (define vp1 (new vertical-panel% [parent hp]))
+  (define vp2 (new vertical-panel% [parent hp]))
+  (define chk (new check-box% 
+                   [label "Show diff"]
+                   [parent f]
+                   [callback
+                    (λ (_1 _2)
+                      (cond
+                        [(send chk get-value)
+                         (send right-hand set-label diff-bitmap)]
+                        [else
+                         (send right-hand set-label new-bitmap)]))]))
+  (define btn (new button%
+                   [parent f]
+                   [label "Save"]
+                   [callback
+                    (λ (x y)
+                      (send new-bitmap save-file filename 'png))]))
+  (define left-label (new message% [parent vp1] [label "Old"]))
+  (define left-hand (new message%
+                         [parent vp1]
+                         [label diff-bitmap]))
+  (define right-label (new message% [parent vp2] [label "New"]))
+  (define right-hand (new message%
+                          [parent vp2]
+                          [label diff-bitmap]))
+  (send left-hand set-label old-bitmap)
+  (send right-hand set-label new-bitmap)
+  f)
diff --git a/collects/redex/private/bmps-macosx/extended-language.png b/collects/redex/private/bmps-macosx/extended-language.png
new file mode 100644
index 0000000000..448f4f9bfb
Binary files /dev/null and b/collects/redex/private/bmps-macosx/extended-language.png differ
diff --git a/collects/redex/private/bmps-macosx/extended-reduction-relation.png b/collects/redex/private/bmps-macosx/extended-reduction-relation.png
new file mode 100644
index 0000000000..46e14cf703
Binary files /dev/null and b/collects/redex/private/bmps-macosx/extended-reduction-relation.png differ
diff --git a/collects/redex/private/bmps-macosx/language-nox.png b/collects/redex/private/bmps-macosx/language-nox.png
new file mode 100644
index 0000000000..083d80cc66
Binary files /dev/null and b/collects/redex/private/bmps-macosx/language-nox.png differ
diff --git a/collects/redex/private/bmps-macosx/language.png b/collects/redex/private/bmps-macosx/language.png
new file mode 100644
index 0000000000..1275c7b26c
Binary files /dev/null and b/collects/redex/private/bmps-macosx/language.png differ
diff --git a/collects/redex/private/bmps-macosx/lw.png b/collects/redex/private/bmps-macosx/lw.png
new file mode 100644
index 0000000000..7a93ada00e
Binary files /dev/null and b/collects/redex/private/bmps-macosx/lw.png differ
diff --git a/collects/redex/private/bmps-macosx/metafunction-Name-vertical.png b/collects/redex/private/bmps-macosx/metafunction-Name-vertical.png
new file mode 100644
index 0000000000..631aa05f6d
Binary files /dev/null and b/collects/redex/private/bmps-macosx/metafunction-Name-vertical.png differ
diff --git a/collects/redex/private/bmps-macosx/metafunction-Name.png b/collects/redex/private/bmps-macosx/metafunction-Name.png
new file mode 100644
index 0000000000..e4f7dc5331
Binary files /dev/null and b/collects/redex/private/bmps-macosx/metafunction-Name.png differ
diff --git a/collects/redex/private/bmps-macosx/metafunction-T.png b/collects/redex/private/bmps-macosx/metafunction-T.png
new file mode 100644
index 0000000000..23606d0bd5
Binary files /dev/null and b/collects/redex/private/bmps-macosx/metafunction-T.png differ
diff --git a/collects/redex/private/bmps-macosx/metafunction-TL.png b/collects/redex/private/bmps-macosx/metafunction-TL.png
new file mode 100644
index 0000000000..1b0410ede7
Binary files /dev/null and b/collects/redex/private/bmps-macosx/metafunction-TL.png differ
diff --git a/collects/redex/private/bmps-macosx/metafunction-multi-arg.png b/collects/redex/private/bmps-macosx/metafunction-multi-arg.png
new file mode 100644
index 0000000000..0ae325b3b0
Binary files /dev/null and b/collects/redex/private/bmps-macosx/metafunction-multi-arg.png differ
diff --git a/collects/redex/private/bmps-macosx/metafunction-subst.png b/collects/redex/private/bmps-macosx/metafunction-subst.png
new file mode 100644
index 0000000000..bf2dbc48f6
Binary files /dev/null and b/collects/redex/private/bmps-macosx/metafunction-subst.png differ
diff --git a/collects/redex/private/bmps-macosx/metafunction.png b/collects/redex/private/bmps-macosx/metafunction.png
new file mode 100644
index 0000000000..5eb6cdbeff
Binary files /dev/null and b/collects/redex/private/bmps-macosx/metafunction.png differ
diff --git a/collects/redex/private/bmps-macosx/metafunctions-multiple.png b/collects/redex/private/bmps-macosx/metafunctions-multiple.png
new file mode 100644
index 0000000000..84b93559ce
Binary files /dev/null and b/collects/redex/private/bmps-macosx/metafunctions-multiple.png differ
diff --git a/collects/redex/private/bmps-macosx/red2.png b/collects/redex/private/bmps-macosx/red2.png
new file mode 100644
index 0000000000..6dfe8ab649
Binary files /dev/null and b/collects/redex/private/bmps-macosx/red2.png differ
diff --git a/collects/redex/private/bmps-macosx/reduction-relation.png b/collects/redex/private/bmps-macosx/reduction-relation.png
new file mode 100644
index 0000000000..1da77851c2
Binary files /dev/null and b/collects/redex/private/bmps-macosx/reduction-relation.png differ
diff --git a/collects/redex/private/bmps/unix-extended-language.png b/collects/redex/private/bmps-macosx/unix-extended-language.png
similarity index 100%
rename from collects/redex/private/bmps/unix-extended-language.png
rename to collects/redex/private/bmps-macosx/unix-extended-language.png
diff --git a/collects/redex/private/bmps/unix-extended-reduction-relation.png b/collects/redex/private/bmps-macosx/unix-extended-reduction-relation.png
similarity index 100%
rename from collects/redex/private/bmps/unix-extended-reduction-relation.png
rename to collects/redex/private/bmps-macosx/unix-extended-reduction-relation.png
diff --git a/collects/redex/private/bmps/unix-language-nox.png b/collects/redex/private/bmps-macosx/unix-language-nox.png
similarity index 100%
rename from collects/redex/private/bmps/unix-language-nox.png
rename to collects/redex/private/bmps-macosx/unix-language-nox.png
diff --git a/collects/redex/private/bmps/unix-language.png b/collects/redex/private/bmps-macosx/unix-language.png
similarity index 100%
rename from collects/redex/private/bmps/unix-language.png
rename to collects/redex/private/bmps-macosx/unix-language.png
diff --git a/collects/redex/private/bmps/unix-lw.png b/collects/redex/private/bmps-macosx/unix-lw.png
similarity index 100%
rename from collects/redex/private/bmps/unix-lw.png
rename to collects/redex/private/bmps-macosx/unix-lw.png
diff --git a/collects/redex/private/bmps/unix-metafunction-Name-vertical.png b/collects/redex/private/bmps-macosx/unix-metafunction-Name-vertical.png
similarity index 100%
rename from collects/redex/private/bmps/unix-metafunction-Name-vertical.png
rename to collects/redex/private/bmps-macosx/unix-metafunction-Name-vertical.png
diff --git a/collects/redex/private/bmps/unix-metafunction-Name.png b/collects/redex/private/bmps-macosx/unix-metafunction-Name.png
similarity index 100%
rename from collects/redex/private/bmps/unix-metafunction-Name.png
rename to collects/redex/private/bmps-macosx/unix-metafunction-Name.png
diff --git a/collects/redex/private/bmps/unix-metafunction-T.png b/collects/redex/private/bmps-macosx/unix-metafunction-T.png
similarity index 100%
rename from collects/redex/private/bmps/unix-metafunction-T.png
rename to collects/redex/private/bmps-macosx/unix-metafunction-T.png
diff --git a/collects/redex/private/bmps/unix-metafunction-TL.png b/collects/redex/private/bmps-macosx/unix-metafunction-TL.png
similarity index 100%
rename from collects/redex/private/bmps/unix-metafunction-TL.png
rename to collects/redex/private/bmps-macosx/unix-metafunction-TL.png
diff --git a/collects/redex/private/bmps/unix-metafunction-multi-arg.png b/collects/redex/private/bmps-macosx/unix-metafunction-multi-arg.png
similarity index 100%
rename from collects/redex/private/bmps/unix-metafunction-multi-arg.png
rename to collects/redex/private/bmps-macosx/unix-metafunction-multi-arg.png
diff --git a/collects/redex/private/bmps/unix-metafunction-subst.png b/collects/redex/private/bmps-macosx/unix-metafunction-subst.png
similarity index 100%
rename from collects/redex/private/bmps/unix-metafunction-subst.png
rename to collects/redex/private/bmps-macosx/unix-metafunction-subst.png
diff --git a/collects/redex/private/bmps/unix-metafunction.png b/collects/redex/private/bmps-macosx/unix-metafunction.png
similarity index 100%
rename from collects/redex/private/bmps/unix-metafunction.png
rename to collects/redex/private/bmps-macosx/unix-metafunction.png
diff --git a/collects/redex/private/bmps/unix-metafunctions-multiple.png b/collects/redex/private/bmps-macosx/unix-metafunctions-multiple.png
similarity index 100%
rename from collects/redex/private/bmps/unix-metafunctions-multiple.png
rename to collects/redex/private/bmps-macosx/unix-metafunctions-multiple.png
diff --git a/collects/redex/private/bmps/unix-reduction-relation.png b/collects/redex/private/bmps-macosx/unix-reduction-relation.png
similarity index 100%
rename from collects/redex/private/bmps/unix-reduction-relation.png
rename to collects/redex/private/bmps-macosx/unix-reduction-relation.png
diff --git a/collects/redex/private/bmps/extended-language.png b/collects/redex/private/bmps/extended-language.png
deleted file mode 100644
index 117dcc482c..0000000000
Binary files a/collects/redex/private/bmps/extended-language.png and /dev/null differ
diff --git a/collects/redex/private/bmps/extended-reduction-relation.png b/collects/redex/private/bmps/extended-reduction-relation.png
deleted file mode 100644
index 057be006b3..0000000000
Binary files a/collects/redex/private/bmps/extended-reduction-relation.png and /dev/null differ
diff --git a/collects/redex/private/bmps/language-nox.png b/collects/redex/private/bmps/language-nox.png
deleted file mode 100644
index 107fbde941..0000000000
Binary files a/collects/redex/private/bmps/language-nox.png and /dev/null differ
diff --git a/collects/redex/private/bmps/language.png b/collects/redex/private/bmps/language.png
deleted file mode 100644
index bd786cb6c7..0000000000
Binary files a/collects/redex/private/bmps/language.png and /dev/null differ
diff --git a/collects/redex/private/bmps/lw.png b/collects/redex/private/bmps/lw.png
deleted file mode 100644
index 19acca0dfa..0000000000
Binary files a/collects/redex/private/bmps/lw.png and /dev/null differ
diff --git a/collects/redex/private/bmps/metafunction-Name-vertical.png b/collects/redex/private/bmps/metafunction-Name-vertical.png
deleted file mode 100644
index 6d1d9f74ce..0000000000
Binary files a/collects/redex/private/bmps/metafunction-Name-vertical.png and /dev/null differ
diff --git a/collects/redex/private/bmps/metafunction-Name.png b/collects/redex/private/bmps/metafunction-Name.png
deleted file mode 100644
index 989837fdae..0000000000
Binary files a/collects/redex/private/bmps/metafunction-Name.png and /dev/null differ
diff --git a/collects/redex/private/bmps/metafunction-T.png b/collects/redex/private/bmps/metafunction-T.png
deleted file mode 100644
index 5de053d89e..0000000000
Binary files a/collects/redex/private/bmps/metafunction-T.png and /dev/null differ
diff --git a/collects/redex/private/bmps/metafunction-TL.png b/collects/redex/private/bmps/metafunction-TL.png
deleted file mode 100644
index 81a744f06d..0000000000
Binary files a/collects/redex/private/bmps/metafunction-TL.png and /dev/null differ
diff --git a/collects/redex/private/bmps/metafunction-multi-arg.png b/collects/redex/private/bmps/metafunction-multi-arg.png
deleted file mode 100644
index f4f2aa2c40..0000000000
Binary files a/collects/redex/private/bmps/metafunction-multi-arg.png and /dev/null differ
diff --git a/collects/redex/private/bmps/metafunction-subst.png b/collects/redex/private/bmps/metafunction-subst.png
deleted file mode 100644
index 6cea486ecb..0000000000
Binary files a/collects/redex/private/bmps/metafunction-subst.png and /dev/null differ
diff --git a/collects/redex/private/bmps/metafunction.png b/collects/redex/private/bmps/metafunction.png
deleted file mode 100644
index 6182623eec..0000000000
Binary files a/collects/redex/private/bmps/metafunction.png and /dev/null differ
diff --git a/collects/redex/private/bmps/metafunctions-multiple.png b/collects/redex/private/bmps/metafunctions-multiple.png
deleted file mode 100644
index 52cfefea28..0000000000
Binary files a/collects/redex/private/bmps/metafunctions-multiple.png and /dev/null differ
diff --git a/collects/redex/private/bmps/reduction-relation.png b/collects/redex/private/bmps/reduction-relation.png
deleted file mode 100644
index aac5e1afa0..0000000000
Binary files a/collects/redex/private/bmps/reduction-relation.png and /dev/null differ
diff --git a/collects/redex/private/config.ss b/collects/redex/private/config.ss
new file mode 100644
index 0000000000..721ab32da1
--- /dev/null
+++ b/collects/redex/private/config.ss
@@ -0,0 +1,5 @@
+#lang scheme
+(provide set-show-bitmaps? get-show-bitmaps?)
+(define show-bitmaps? #t)
+(define (set-show-bitmaps? sb?) (set! show-bitmaps? sb?))
+(define (get-show-bitmaps?) show-bitmaps?)
\ No newline at end of file
diff --git a/collects/redex/private/reduction-semantics.ss b/collects/redex/private/reduction-semantics.ss
index f881734bf8..5c6ee9b464 100644
--- a/collects/redex/private/reduction-semantics.ss
+++ b/collects/redex/private/reduction-semantics.ss
@@ -220,76 +220,73 @@
 
 ;; the withs, freshs, and side-conditions come in backwards order
 (define-for-syntax (bind-withs orig-name main lang lang-nts stx where-mode body)
-  (let loop ([stx stx]
-             [body body]
-             [bindings '()])
-    (syntax-case stx (side-condition where fresh)
-      [() (values body bindings)]
-      [((where x e) y ...)
-       (let-values ([(names names/ellipses) (extract-names lang-nts 'reduction-relation #t #'x)])
-         (with-syntax ([(cpat) (generate-temporaries '(compiled-pattern))]
-                       [side-conditions-rewritten (rewrite-side-conditions/check-errs
-                                                   lang-nts
-                                                   'reduction-relation
-                                                   #f
-                                                   #'x)]
-                       [(names ...) names]
-                       [(names/ellipses ...) names/ellipses])
-           (loop #'(y ...) 
-                 #`(let ([mtchs (match-pattern cpat (term e))])
-                     (if mtchs
-                         #,
-                         (case where-mode
-                           [(flatten)
-                            #`(apply
-                               append
-                               (map (λ (mtch)
-                                      (let ([bindings (mtch-bindings mtch)])
-                                        (term-let ([names/ellipses (lookup-binding bindings 'names)] ...) 
-                                                  #,body)))
-                                    mtchs))]
-                           [(predicate) 
-                            #`(andmap (λ (mtch)
-                                        (let ([bindings (mtch-bindings mtch)])
-                                          (term-let ([names/ellipses (lookup-binding bindings 'names)] ...) 
-                                                    #,body)))
-                                      mtchs)]
-                           [else (error 'unknown-where-mode "~s" where-mode)])
-                         #f))
-                 (cons #`[cpat (compile-pattern #,lang `side-conditions-rewritten #t)]
-                       bindings))))]
-      [((side-condition s ...) y ...)
-       (loop #'(y ...) #`(and s ... #,body) bindings)]
-      [((fresh x) y ...)
-       (identifier? #'x)
-       (loop #'(y ...) 
-             #`(term-let ([x (variable-not-in #,main 'x)]) #,body)
-             bindings)]
-      [((fresh x name) y ...)
-       (identifier? #'x)
-       (loop #'(y ...)
-             #`(term-let ([x (let ([the-name (term name)])
-                               (verify-name-ok '#,orig-name the-name)
-                               (variable-not-in #,main the-name))])
-                         #,body)
-             bindings)]
-      [((fresh (y) (x ...)) z ...)
-       (loop #'(z ...)
-             #`(term-let ([(y #,'...)
-                           (variables-not-in #,main 
-                                             (map (λ (_ignore_) 'y)
-                                                  (term (x ...))))])
-                         #,body)
-             bindings)]
-      [((fresh (y) (x ...) names) z ...)
-       (loop #'(z ...)
-             #`(term-let ([(y #,'...)
-                           (let ([the-names (term names)]
-                                 [len-counter (term (x ...))])
-                             (verify-names-ok '#,orig-name the-names len-counter)
-                             (variables-not-in #,main the-names))])
-                         #,body)
-             bindings)])))
+  (let* ([bindings '()]
+         [body
+          (let loop ([stx stx]
+                     [to-not-be-in main])
+            (syntax-case stx (side-condition where fresh)
+              [() body]
+              [((where x e) y ...)
+               (let-values ([(names names/ellipses) (extract-names lang-nts 'reduction-relation #t #'x)])
+                 (with-syntax ([(cpat) (generate-temporaries '(compiled-pattern))]
+                               [side-conditions-rewritten (rewrite-side-conditions/check-errs
+                                                           lang-nts
+                                                           'reduction-relation
+                                                           #f
+                                                           #'x)]
+                               [(names ...) names]
+                               [(names/ellipses ...) names/ellipses])
+                   (with-syntax ([(x ...) (generate-temporaries #'(names ...))])
+                     (set! bindings (cons #`[cpat (compile-pattern #,lang `side-conditions-rewritten #t)] bindings))
+                     (let ([rest-body (loop #'(y ...) #`(list x ... #,to-not-be-in))])
+                       #`(let ([mtchs (match-pattern cpat (term e))])
+                           (if mtchs
+                               #,
+                               (case where-mode
+                                 [(flatten)
+                                  #`(apply
+                                     append
+                                     (map (λ (mtch)
+                                            (let ([bindings (mtch-bindings mtch)])
+                                              (let ([x (lookup-binding bindings 'names)] ...)
+                                                (term-let ([names/ellipses x] ...) 
+                                                          #,rest-body))))
+                                          mtchs))]
+                                 [(predicate) 
+                                  #`(andmap (λ (mtch)
+                                              (let ([bindings (mtch-bindings mtch)])
+                                                (let ([x (lookup-binding bindings 'names)] ...)
+                                                  (term-let ([names/ellipses x] ...) 
+                                                            #,rest-body))))
+                                            mtchs)]
+                                 [else (error 'unknown-where-mode "~s" where-mode)])
+                               #f))))))]
+              [((side-condition s ...) y ...)
+               #`(and s ... #,(loop #'(y ...) to-not-be-in))]
+              [((fresh x) y ...)
+               (identifier? #'x)
+               #`(term-let ([x (variable-not-in #,to-not-be-in 'x)]) 
+                           #,(loop #'(y ...) #`(list (term x) #,to-not-be-in)))]
+              [((fresh x name) y ...)
+               (identifier? #'x)
+               #`(term-let ([x (let ([the-name (term name)])
+                                 (verify-name-ok '#,orig-name the-name)
+                                 (variable-not-in #,to-not-be-in the-name))])
+                           #,(loop #'(y ...) #`(list (term x) #,to-not-be-in)))]
+              [((fresh (y) (x ...)) z ...)
+               #`(term-let ([(y #,'...)
+                             (variables-not-in #,to-not-be-in 
+                                               (map (λ (_ignore_) 'y)
+                                                    (term (x ...))))])
+                           #,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in)))]
+              [((fresh (y) (x ...) names) z ...)
+               #`(term-let ([(y #,'...)
+                             (let ([the-names (term names)]
+                                   [len-counter (term (x ...))])
+                               (verify-names-ok '#,orig-name the-names len-counter)
+                               (variables-not-in #,to-not-be-in the-names))])
+                           #,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in)))]))])
+    (values body bindings)))
 
 (define-syntax-set (do-reduction-relation)
   (define (do-reduction-relation/proc stx)
@@ -746,84 +743,76 @@
                case-id)))))))
   
   (define (process-extras stx orig-name name-table extras)
-    (let ([the-name #f]
-          [the-name-stx #f]
-          [sides/withs/freshs '()])
-      (let loop ([extras extras])
-        (cond
-          [(null? extras) (values the-name sides/withs/freshs)]
-          [else
-           (syntax-case (car extras) (side-condition fresh where)
-             [name 
-              (or (identifier? (car extras))
-                  (string? (syntax-e (car extras))))
-              (begin
-                (let* ([raw-name (syntax-e (car extras))]
-                       [name-sym
-                        (if (symbol? raw-name)
-                            raw-name
-                            (string->symbol raw-name))])
-                  (when (hash-ref name-table name-sym #f)
-                    (raise-syntax-errors orig-name 
-                                         "same name on multiple rules"
-                                         stx
-                                         (list (car (hash-ref name-table name-sym))
-                                               (syntax name))))
-                  (let ([num (hash-ref name-table #f)])
-                    (hash-set! name-table #f (+ num 1))
-                    (hash-set! name-table name-sym (list (syntax name) num)))
-                  
-                  (when the-name
-                    (raise-syntax-errors orig-name
-                                         "expected only a single name" 
-                                         stx
-                                         (list the-name-stx (car extras))))
-                  (set! the-name (if (symbol? raw-name)
-                                     (symbol->string raw-name)
-                                     raw-name))
-                  (set! the-name-stx (car extras))
-                  (loop (cdr extras))))]
-             [(fresh var ...)
-              (begin
-                (set! sides/withs/freshs
-                      (append 
-                       (reverse 
-                        (map (λ (x)
-                               (syntax-case x ()
-                                 [x
-                                  (identifier? #'x)
-                                  #'(fresh x)]
-                                 [(x name)
-                                  (identifier? #'x)
-                                  #'(fresh x name)]
-                                 [((ys dots2) (xs dots1))
-                                  (and (eq? (syntax-e #'dots1) (string->symbol "..."))
-                                       (eq? (syntax-e #'dots2) (string->symbol "...")))
-                                  #'(fresh (ys) (xs dots1))]
-                                 [((ys dots2) (xs dots1) names)
-                                  (and (eq? (syntax-e #'dots1) (string->symbol "..."))
-                                       (eq? (syntax-e #'dots2) (string->symbol "...")))
-                                  #'(fresh (ys) (xs dots1) names)]
-                                 [x
-                                  (raise-syntax-error orig-name 
-                                                      "malformed fresh variable clause"
-                                                      stx
-                                                      #'x)]))
-                             (syntax->list #'(var ...))))
-                       sides/withs/freshs))
-                (loop (cdr extras)))]
-             [(side-condition exp ...)
-              (begin 
-                (set! sides/withs/freshs (cons (car extras) sides/withs/freshs))
-                (loop (cdr extras)))]
-             [(where x e)
-              (begin
-                (set! sides/withs/freshs (cons (car extras) sides/withs/freshs))
-                (loop (cdr extras)))]
-             [(where . x)
-              (raise-syntax-error orig-name "malformed where clause" stx (car extras))]
-             [_
-              (raise-syntax-error orig-name "unknown extra" stx (car extras))])]))))
+    (let* ([the-name #f]
+           [the-name-stx #f]
+           [sides/withs/freshs 
+            (let loop ([extras extras])
+              (cond
+                [(null? extras) '()]
+                [else
+                 (syntax-case (car extras) (side-condition fresh where)
+                   [name 
+                    (or (identifier? (car extras))
+                        (string? (syntax-e (car extras))))
+                    (begin
+                      (let* ([raw-name (syntax-e (car extras))]
+                             [name-sym
+                              (if (symbol? raw-name)
+                                  raw-name
+                                  (string->symbol raw-name))])
+                        (when (hash-ref name-table name-sym #f)
+                          (raise-syntax-errors orig-name 
+                                               "same name on multiple rules"
+                                               stx
+                                               (list (car (hash-ref name-table name-sym))
+                                                     (syntax name))))
+                        (let ([num (hash-ref name-table #f)])
+                          (hash-set! name-table #f (+ num 1))
+                          (hash-set! name-table name-sym (list (syntax name) num)))
+                        
+                        (when the-name
+                          (raise-syntax-errors orig-name
+                                               "expected only a single name" 
+                                               stx
+                                               (list the-name-stx (car extras))))
+                        (set! the-name (if (symbol? raw-name)
+                                           (symbol->string raw-name)
+                                           raw-name))
+                        (set! the-name-stx (car extras))
+                        (loop (cdr extras))))]
+                   [(fresh var ...)
+                    (append (map (λ (x)
+                                   (syntax-case x ()
+                                     [x
+                                      (identifier? #'x)
+                                      #'(fresh x)]
+                                     [(x name)
+                                      (identifier? #'x)
+                                      #'(fresh x name)]
+                                     [((ys dots2) (xs dots1))
+                                      (and (eq? (syntax-e #'dots1) (string->symbol "..."))
+                                           (eq? (syntax-e #'dots2) (string->symbol "...")))
+                                      #'(fresh (ys) (xs dots1))]
+                                     [((ys dots2) (xs dots1) names)
+                                      (and (eq? (syntax-e #'dots1) (string->symbol "..."))
+                                           (eq? (syntax-e #'dots2) (string->symbol "...")))
+                                      #'(fresh (ys) (xs dots1) names)]
+                                     [x
+                                      (raise-syntax-error orig-name 
+                                                          "malformed fresh variable clause"
+                                                          stx
+                                                          #'x)]))
+                                 (syntax->list #'(var ...)))
+                            (loop (cdr extras)))]
+                   [(side-condition exp ...)
+                    (cons (car extras) (loop (cdr extras)))]
+                   [(where x e)
+                    (cons (car extras) (loop (cdr extras)))]
+                   [(where . x)
+                    (raise-syntax-error orig-name "malformed where clause" stx (car extras))]
+                   [_
+                    (raise-syntax-error orig-name "unknown extra" stx (car extras))])]))])
+      (values the-name sides/withs/freshs)))
   
 
   
@@ -1125,182 +1114,178 @@
                                              (list name
                                                    (car names)))))
                                          (loop name (cdr names))]))])
-                  
-                  (with-syntax ([(((tl-side-conds ...) ...) 
-                                  (tl-bindings ...)
-                                  (tl-side-cond/binds ...))
-                                 (parse-extras #'((stuff ...) ...))])
-                      (with-syntax ([(((cp-let-bindings ...) rhs/wheres) ...)
-                                     (map (λ (sc/b rhs)
-                                            (let-values ([(body-code cp-let-bindings) 
-                                                          (bind-withs
-                                                           syn-error-name '()  
-                                                           #'lang lang-nts
-                                                           sc/b 'flatten
-                                                           #`(list (term #,rhs)))])
-                                              (list cp-let-bindings body-code)))
-                                          (syntax->list #'(tl-side-cond/binds ...))
-                                          (syntax->list #'(rhs ...)))]
-                                    [(((rg-cp-let-bindings ...) rg-rhs/wheres) ...)
-                                     (map (λ (sc/b rhs) 
-                                            (let-values ([(body-code cp-let-bindings) 
-                                                          (bind-withs
-                                                           syn-error-name '()  
-                                                           #'lang lang-nts
-                                                           sc/b 'predicate
-                                                           #`#t)])
-                                              (list cp-let-bindings body-code)))
-                                          (syntax->list #'(tl-side-cond/binds ...))
-                                          (syntax->list #'(rhs ...)))])
-                        (with-syntax ([(side-conditions-rewritten ...) 
-                                       (map (λ (x) (rewrite-side-conditions/check-errs
-                                                    lang-nts
-                                                    syn-error-name
-                                                    #t
-                                                    x))
-                                            (syntax->list (syntax (lhs ...))))]
-                                      [(rg-side-conditions-rewritten ...) 
-                                       (map (λ (x) (rewrite-side-conditions/check-errs
-                                                    lang-nts
-                                                    syn-error-name
-                                                    #t
-                                                    x))
-                                            (syntax->list (syntax ((side-condition lhs rg-rhs/wheres) ...))))]
-                                      [(clause-src ...)
-                                       (map (λ (lhs)
-                                              (format "~a:~a:~a"
-                                                      (syntax-source lhs)
-                                                      (syntax-line lhs)
-                                                      (syntax-column lhs)))
-                                            pats)]
-                                      [dom-side-conditions-rewritten
-                                       (and dom-ctcs
-                                            (rewrite-side-conditions/check-errs
-                                             lang-nts
-                                             syn-error-name
-                                             #f
-                                             dom-ctcs))]
-                                      [codom-side-conditions-rewritten
-                                       (rewrite-side-conditions/check-errs
-                                        lang-nts
-                                        syn-error-name
-                                        #f
-                                        codom-contract)]
-                                      [(rhs-fns ...)
-                                       (map (λ (lhs rhs/where)
-                                              (let-values ([(names names/ellipses) 
-                                                            (extract-names lang-nts syn-error-name #t lhs)])
-                                                (with-syntax ([(names ...) names]
-                                                              [(names/ellipses ...) names/ellipses]
-                                                              [rhs/where rhs/where])
-                                                  (syntax
-                                                   (λ (name bindings)
-                                                     (term-let-fn ((name name))
-                                                                  (term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
-                                                                            rhs/where)))))))
-                                            (syntax->list (syntax (lhs ...)))
-                                            (syntax->list (syntax (rhs/wheres ...))))]
-                                      [(name2 name-predicate) (generate-temporaries (syntax (name name)))]
-
-                                      ;; See "!!" below for information on the `seq-' bindings:
-                                      [seq-of-rhs #'(rhs ...)]
-                                      [seq-of-lhs #'(lhs ...)]
-                                      [seq-of-tl-side-cond/binds #'(tl-side-cond/binds ...)]
-                                      [seq-of-lhs-for-lw #'(lhs-for-lw ...)])
-                          (with-syntax ([defs #`(begin
-                                                  (define-values (name2 name-predicate)
-                                                    (let ([sc `(side-conditions-rewritten ...)]
-                                                          [dsc `dom-side-conditions-rewritten]
-                                                          cp-let-bindings ... ...
-                                                          rg-cp-let-bindings ... ...)
-                                                      (let ([cases (map (λ (pat rhs-fn rg-lhs src)
-                                                                          (make-metafunc-case
-                                                                           (compile-pattern lang pat #t) rhs-fn rg-lhs src (gensym)))
-                                                                        sc
-                                                                        (list rhs-fns ...)
-                                                                        `(rg-side-conditions-rewritten ...)
-                                                                        `(clause-src ...))]
-                                                            [parent-cases 
-                                                             #,(if prev-metafunction
-                                                                   #`(metafunc-proc-cases #,(term-fn-get-id (syntax-local-value prev-metafunction)))
-                                                                   #'null)])
-                                                        (build-metafunction 
-                                                         lang
-                                                         cases
-                                                         parent-cases
-                                                         (λ (f/dom)
-                                                           (make-metafunc-proc
-                                                            (let ([name (lambda (x) (f/dom x))]) name)
-                                                            ;; !! This code goes back to phase 1 to call `to-lw', but it's delayed
-                                                            ;;    through `let-syntax' instead of `unsyntax' so that `to-lw' isn't called
-                                                            ;;    until all metafunction definitions have been processed.
-                                                            ;;    It gets a little complicated because we want to use sequences from the
-                                                            ;;    original `define-metafunction' (step 1) and sequences that are generated within
-                                                            ;;    `let-syntax' (step 2). So we quote all the `...' in the `let-syntax' form ---
-                                                            ;;    and also have to quote all uses step-1 pattern variables in case they produce
-                                                            ;;    `...', which should be treated as literals at step 2. Hece the `seq-' bindings
-                                                            ;;    above and a quoting `...' on each use of a `seq-' binding.
-                                                            (...
-                                                             (let-syntax 
-                                                                 ([generate-lws
-                                                                   (lambda (stx)
-                                                                     (with-syntax
-                                                                         ([(rhs/lw ...) (map to-lw/proc (syntax->list #'(... seq-of-rhs)))]
-                                                                          [(((bind-id/lw . bind-pat/lw) ...) ...)
-                                                                           ;; Also for pict, extract pattern bindings
-                                                                           (map (λ (x) (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/proc (cdr x))))
-                                                                                            (extract-pattern-binds x)))
-                                                                                (syntax->list #'(... seq-of-lhs)))]
-                                                                          
-                                                                          [((where/sc/lw ...) ...)
-                                                                           ;; Also for pict, extract where bindings
-                                                                           (map (λ (hm)
-                                                                                  (map
-                                                                                   (λ (lst)
-                                                                                     (syntax-case lst (side-condition where)
-                                                                                       [(where pat exp)
-                                                                                        #`(cons #,(to-lw/proc #'pat) #,(to-lw/proc #'exp))]
-                                                                                       [(side-condition x)
-                                                                                        (to-lw/uq/proc #'x)]))
-                                                                                   (reverse (syntax->list hm))))
-                                                                                (syntax->list #'(... seq-of-tl-side-cond/binds)))]
-                                                                          
-                                                                          [(((rhs-bind-id/lw . rhs-bind-pat/lw/uq) ...) ...)
-                                                                           ;; Also for pict, extract pattern bindings
-                                                                           (map (λ (x) (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/uq/proc (cdr x))))
-                                                                                            (extract-term-let-binds x)))
-                                                                                (syntax->list #'(... seq-of-rhs)))]
-                                                                          
-                                                                          [(x-lhs-for-lw ...) #'(... seq-of-lhs-for-lw)])
-                                                                       #'(list (list x-lhs-for-lw
-                                                                                     (list (cons bind-id/lw bind-pat/lw) ...
-                                                                                           (cons rhs-bind-id/lw rhs-bind-pat/lw/uq) ...
-                                                                                           where/sc/lw ...)
-                                                                                     rhs/lw)
-                                                                               ...)))])
-                                                               (generate-lws)))
-                                                            lang
-                                                            #t ;; multi-args?
-                                                            'name
-                                                            (let ([name (lambda (x) (name-predicate x))]) name)
-                                                            dsc
-                                                            (append cases parent-cases)))
-                                                         dsc
-                                                         `codom-side-conditions-rewritten
-                                                         'name
-                                                         #,relation?))))
-                                                  (term-define-fn name name2))])
-                            (syntax-property
-                             (if (eq? 'top-level (syntax-local-context))
-                                 ; Introduce the names before using them, to allow
-                                 ; metafunction definition at the top-level.
-                                 (syntax 
-                                  (begin 
-                                    (define-syntaxes (name2 name-predicate) (values))
-                                    defs))
-                                 (syntax defs))
-                             'disappeared-use
-                             (map syntax-local-introduce (syntax->list #'(original-names ...))))))))))))))))]
+                  (parse-extras #'((stuff ...) ...))
+                    (with-syntax ([(((cp-let-bindings ...) rhs/wheres) ...)
+                                   (map (λ (sc/b rhs)
+                                          (let-values ([(body-code cp-let-bindings) 
+                                                        (bind-withs
+                                                         syn-error-name '()  
+                                                         #'lang lang-nts
+                                                         sc/b 'flatten
+                                                         #`(list (term #,rhs)))])
+                                            (list cp-let-bindings body-code)))
+                                        (syntax->list #'((stuff ...) ...))
+                                        (syntax->list #'(rhs ...)))]
+                                  [(((rg-cp-let-bindings ...) rg-rhs/wheres) ...)
+                                   (map (λ (sc/b rhs) 
+                                          (let-values ([(body-code cp-let-bindings) 
+                                                        (bind-withs
+                                                         syn-error-name '()  
+                                                         #'lang lang-nts
+                                                         sc/b 'predicate
+                                                         #`#t)])
+                                            (list cp-let-bindings body-code)))
+                                        (syntax->list #'((stuff ...) ...))
+                                        (syntax->list #'(rhs ...)))])
+                      (with-syntax ([(side-conditions-rewritten ...) 
+                                     (map (λ (x) (rewrite-side-conditions/check-errs
+                                                  lang-nts
+                                                  syn-error-name
+                                                  #t
+                                                  x))
+                                          (syntax->list (syntax (lhs ...))))]
+                                    [(rg-side-conditions-rewritten ...) 
+                                     (map (λ (x) (rewrite-side-conditions/check-errs
+                                                  lang-nts
+                                                  syn-error-name
+                                                  #t
+                                                  x))
+                                          (syntax->list (syntax ((side-condition lhs rg-rhs/wheres) ...))))]
+                                    [(clause-src ...)
+                                     (map (λ (lhs)
+                                            (format "~a:~a:~a"
+                                                    (syntax-source lhs)
+                                                    (syntax-line lhs)
+                                                    (syntax-column lhs)))
+                                          pats)]
+                                    [dom-side-conditions-rewritten
+                                     (and dom-ctcs
+                                          (rewrite-side-conditions/check-errs
+                                           lang-nts
+                                           syn-error-name
+                                           #f
+                                           dom-ctcs))]
+                                    [codom-side-conditions-rewritten
+                                     (rewrite-side-conditions/check-errs
+                                      lang-nts
+                                      syn-error-name
+                                      #f
+                                      codom-contract)]
+                                    [(rhs-fns ...)
+                                     (map (λ (lhs rhs/where)
+                                            (let-values ([(names names/ellipses) 
+                                                          (extract-names lang-nts syn-error-name #t lhs)])
+                                              (with-syntax ([(names ...) names]
+                                                            [(names/ellipses ...) names/ellipses]
+                                                            [rhs/where rhs/where])
+                                                (syntax
+                                                 (λ (name bindings)
+                                                   (term-let-fn ((name name))
+                                                                (term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
+                                                                          rhs/where)))))))
+                                          (syntax->list (syntax (lhs ...)))
+                                          (syntax->list (syntax (rhs/wheres ...))))]
+                                    [(name2 name-predicate) (generate-temporaries (syntax (name name)))]
+                                    
+                                    ;; See "!!" below for information on the `seq-' bindings:
+                                    [seq-of-rhs #'(rhs ...)]
+                                    [seq-of-lhs #'(lhs ...)]
+                                    [seq-of-tl-side-cond/binds #'((stuff ...) ...)]
+                                    [seq-of-lhs-for-lw #'(lhs-for-lw ...)])
+                        (with-syntax ([defs #`(begin
+                                                (define-values (name2 name-predicate)
+                                                  (let ([sc `(side-conditions-rewritten ...)]
+                                                        [dsc `dom-side-conditions-rewritten]
+                                                        cp-let-bindings ... ...
+                                                        rg-cp-let-bindings ... ...)
+                                                    (let ([cases (map (λ (pat rhs-fn rg-lhs src)
+                                                                        (make-metafunc-case
+                                                                         (compile-pattern lang pat #t) rhs-fn rg-lhs src (gensym)))
+                                                                      sc
+                                                                      (list rhs-fns ...)
+                                                                      `(rg-side-conditions-rewritten ...)
+                                                                      `(clause-src ...))]
+                                                          [parent-cases 
+                                                           #,(if prev-metafunction
+                                                                 #`(metafunc-proc-cases #,(term-fn-get-id (syntax-local-value prev-metafunction)))
+                                                                 #'null)])
+                                                      (build-metafunction 
+                                                       lang
+                                                       cases
+                                                       parent-cases
+                                                       (λ (f/dom)
+                                                         (make-metafunc-proc
+                                                          (let ([name (lambda (x) (f/dom x))]) name)
+                                                          ;; !! This code goes back to phase 1 to call `to-lw', but it's delayed
+                                                          ;;    through `let-syntax' instead of `unsyntax' so that `to-lw' isn't called
+                                                          ;;    until all metafunction definitions have been processed.
+                                                          ;;    It gets a little complicated because we want to use sequences from the
+                                                          ;;    original `define-metafunction' (step 1) and sequences that are generated within
+                                                          ;;    `let-syntax' (step 2). So we quote all the `...' in the `let-syntax' form ---
+                                                          ;;    and also have to quote all uses step-1 pattern variables in case they produce
+                                                          ;;    `...', which should be treated as literals at step 2. Hece the `seq-' bindings
+                                                          ;;    above and a quoting `...' on each use of a `seq-' binding.
+                                                          (...
+                                                           (let-syntax 
+                                                               ([generate-lws
+                                                                 (lambda (stx)
+                                                                   (with-syntax
+                                                                       ([(rhs/lw ...) (map to-lw/proc (syntax->list #'(... seq-of-rhs)))]
+                                                                        [(((bind-id/lw . bind-pat/lw) ...) ...)
+                                                                         ;; Also for pict, extract pattern bindings
+                                                                         (map (λ (x) (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/proc (cdr x))))
+                                                                                          (extract-pattern-binds x)))
+                                                                              (syntax->list #'(... seq-of-lhs)))]
+                                                                        
+                                                                        [((where/sc/lw ...) ...)
+                                                                         ;; Also for pict, extract where bindings
+                                                                         (map (λ (hm)
+                                                                                (map
+                                                                                 (λ (lst)
+                                                                                   (syntax-case lst (side-condition where)
+                                                                                     [(where pat exp)
+                                                                                      #`(cons #,(to-lw/proc #'pat) #,(to-lw/proc #'exp))]
+                                                                                     [(side-condition x)
+                                                                                      (to-lw/uq/proc #'x)]))
+                                                                                 (reverse (syntax->list hm))))
+                                                                              (syntax->list #'(... seq-of-tl-side-cond/binds)))]
+                                                                        
+                                                                        [(((rhs-bind-id/lw . rhs-bind-pat/lw/uq) ...) ...)
+                                                                         ;; Also for pict, extract pattern bindings
+                                                                         (map (λ (x) (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/uq/proc (cdr x))))
+                                                                                          (extract-term-let-binds x)))
+                                                                              (syntax->list #'(... seq-of-rhs)))]
+                                                                        
+                                                                        [(x-lhs-for-lw ...) #'(... seq-of-lhs-for-lw)])
+                                                                     #'(list (list x-lhs-for-lw
+                                                                                   (list (cons bind-id/lw bind-pat/lw) ...
+                                                                                         (cons rhs-bind-id/lw rhs-bind-pat/lw/uq) ...
+                                                                                         where/sc/lw ...)
+                                                                                   rhs/lw)
+                                                                             ...)))])
+                                                             (generate-lws)))
+                                                          lang
+                                                          #t ;; multi-args?
+                                                          'name
+                                                          (let ([name (lambda (x) (name-predicate x))]) name)
+                                                          dsc
+                                                          (append cases parent-cases)))
+                                                       dsc
+                                                       `codom-side-conditions-rewritten
+                                                       'name
+                                                       #,relation?))))
+                                                (term-define-fn name name2))])
+                          (syntax-property
+                           (if (eq? 'top-level (syntax-local-context))
+                               ; Introduce the names before using them, to allow
+                               ; metafunction definition at the top-level.
+                               (syntax 
+                                (begin 
+                                  (define-syntaxes (name2 name-predicate) (values))
+                                  defs))
+                               (syntax defs))
+                           'disappeared-use
+                           (map syntax-local-introduce (syntax->list #'(original-names ...)))))))))))))))]
       [(_ prev-metafunction name lang clauses ...)
        (begin
          (unless (identifier? #'name)
@@ -1383,41 +1368,25 @@
          (raise-syntax-error syn-error-name "error checking failed.2" stx))]))
   
   (define (parse-extras extras)
-    (let loop ([stuffs (syntax->list extras)]
-               [side-conditionss '()]
-               [bindingss '()]
-               [bothss '()])
-      (cond
-        [(null? stuffs) (list (reverse side-conditionss)
-                              (reverse bindingss)
-                              (reverse bothss))]
-        [else 
-         (let s-loop ([stuff (syntax->list (car stuffs))]
-                      [side-conditions '()]
-                      [bindings '()]
-                      [boths '()])
-           (cond
-             [(null? stuff) (loop (cdr stuffs)
-                                  (cons (reverse side-conditions) side-conditionss)
-                                  (cons (reverse bindings) bindingss)
-                                  ; Want these in reverse order.
-                                  (cons boths bothss))]
-             [else 
-              (syntax-case (car stuff) (where side-condition)
-                [(side-condition tl-side-conds ...) 
-                 (s-loop (cdr stuff)
-                         (append (syntax->list #'(tl-side-conds ...)) side-conditions)
-                         bindings
-                         (cons (car stuff) boths))]
-                [(where x e)
-                 (s-loop (cdr stuff)
-                         side-conditions
-                         (cons #'(x e) bindings)
-                         (cons (car stuff) boths))]
-                [_
-                 (raise-syntax-error 'define-metafunction 
-                                     "expected a side-condition or where clause"
-                                     (car stuff))])]))]))))
+    (for-each
+     (λ (stuffs)
+       (for-each
+        (λ (stuff)
+          (syntax-case stuff (where side-condition)
+            [(side-condition tl-side-conds ...) 
+             (void)]
+            [(where x e)
+             (void)]
+            [(where . args)
+             (raise-syntax-error 'define-metafunction 
+                                 "malformed where clause"
+                                 stuff)]
+            [_
+             (raise-syntax-error 'define-metafunction 
+                                 "expected a side-condition or where clause"
+                                 stuff)]))
+        (syntax->list stuffs)))
+     (syntax->list extras))))
 
 (define (build-metafunction lang cases parent-cases wrap dom-contract-pat codom-contract-pat name relation?)
   (let ([dom-compiled-pattern (and dom-contract-pat (compile-pattern lang dom-contract-pat #f))]
diff --git a/collects/redex/private/run-tests.ss b/collects/redex/private/run-tests.ss
index b93704cb75..4ec5971dc6 100644
--- a/collects/redex/private/run-tests.ss
+++ b/collects/redex/private/run-tests.ss
@@ -1,7 +1,11 @@
 ;; require this file to run all of the test suites for redex.
 
 #lang scheme/base
-(require scheme/runtime-path)
+(require scheme/runtime-path
+         "config.ss"
+         "test-util.ss")
+
+(set-show-bitmaps? #t)
 
 (define test-files
   '("lw-test.ss" 
@@ -17,8 +21,6 @@
 
 (define-runtime-path here ".")
 
-(putenv "PLT_REDEX_TEST_NOSHOW_DIFFS" "yes")
-
 (define (flush)
   ;; these flushes are here for running under cygwin, 
   ;; which somehow makes mzscheme think it isn't using
diff --git a/collects/redex/private/test-util.ss b/collects/redex/private/test-util.ss
index 283a6596a0..491f32af3c 100644
--- a/collects/redex/private/test-util.ss
+++ b/collects/redex/private/test-util.ss
@@ -35,7 +35,9 @@
 
 (define tests 0)
 (define failures 0)
-(define (reset-count) (set! tests 0))
+(define (reset-count) 
+  (set! tests 0)
+  (set! failures 0))
 
 (define (print-tests-passed filename)
   (cond
diff --git a/collects/redex/private/tl-test.ss b/collects/redex/private/tl-test.ss
index d59d570d7c..d70795b1c5 100644
--- a/collects/redex/private/tl-test.ss
+++ b/collects/redex/private/tl-test.ss
@@ -1211,6 +1211,35 @@
                (fresh ((x ...) (variable_1 ...) (variable_1 ...)))))
          '(x y z))
         (list '(x1 y1 z1 x y z)))
+
+  (test (apply-reduction-relation 
+         (reduction-relation 
+          empty-language
+          (--> any (any_y x)
+               (where any_y x)
+               (fresh x)))
+         (term junk))
+        (list '(x x1)))
+  
+  (test (apply-reduction-relation 
+         (reduction-relation 
+          empty-language
+          (--> any (any_y x)
+               (fresh x)
+               (where any_y x)
+               (fresh x)))
+         (term junk))
+        (list '(x x1)))
+  
+  (test (apply-reduction-relation 
+         (reduction-relation 
+          empty-language
+          (--> (variable ...) (variable_0 ... variable_1 ...)
+               (fresh ((variable_0 ...) (variable ...)))
+               (fresh ((variable_1 ...) (variable ...)))))
+         (term (x y)))
+        (list '(variable_0 variable_1 variable_2 variable_3)))
+
   
   ;; test that redex match can be used in a side-condition 
   ;; with the same language that is used to define the