diff --git a/collects/redex/private/bitmap-test.ss b/collects/redex/private/bitmap-test.ss
index 8d84edfcb6..7f92db36d4 100644
--- a/collects/redex/private/bitmap-test.ss
+++ b/collects/redex/private/bitmap-test.ss
@@ -92,6 +92,7 @@
         (render-metafunction Name))
       "metafunction-Name-vertical.png")
 
+
 ;; makes sure that there is no overlap inside or across metafunction calls  
 ;; or when there are unquotes involved
 (define-metafunction lang
diff --git a/collects/redex/private/core-layout.ss b/collects/redex/private/core-layout.ss
index 5125fb3686..11f938d39d 100644
--- a/collects/redex/private/core-layout.ss
+++ b/collects/redex/private/core-layout.ss
@@ -457,7 +457,12 @@
            (set! current-line line)
            (set! current-column col))]
         [else
-         (error 'eject "lines going backwards")])
+         (error 'eject
+                "lines going backwards (current-line ~s line ~s atom ~s tokens ~s)" 
+                current-line
+                line
+                atom
+                tokens)])
       (when (< current-column col)
         (let ([space-span (- col current-column)])
           (set! tokens (cons (make-blank-space-token unquoted?
diff --git a/collects/redex/private/loc-wrapper-ct.ss b/collects/redex/private/loc-wrapper-ct.ss
new file mode 100644
index 0000000000..ecb416b918
--- /dev/null
+++ b/collects/redex/private/loc-wrapper-ct.ss
@@ -0,0 +1,96 @@
+#lang scheme/base
+(require (for-template scheme/base)
+         (for-template "loc-wrapper-rt.ss")
+         "term-fn.ss")
+(provide to-lw/proc to-lw/uq/proc)
+
+(define (process-arg stx quote-depth)
+  (define quoted? (quote-depth . > . 0))
+  (define-values (op cl)
+    (if (syntax? stx)
+        (case (syntax-property stx 'paren-shape)
+          [(#\{) (values "{" "}")]
+          [(#\[) (values "[" "]")]
+          [else (values "(" ")")])
+        (values #f #f)))
+  (define (reader-shorthand arg qd-delta mrk)
+    #`(init-loc-wrapper 
+       (list (init-loc-wrapper #,mrk
+                               #,(syntax-line stx)
+                               #,(syntax-column stx)
+                               #,quoted?)
+             'spring
+             #,(process-arg arg (+ quote-depth qd-delta)))
+       #,(syntax-line stx) 
+       #,(syntax-column stx)
+       #,quoted?))
+  (define (handle-sequence qd-delta)
+    #`(init-loc-wrapper 
+       (list (init-loc-wrapper #,op #,(syntax-line stx) #,(syntax-column stx) #,quoted?)
+             #,@(map (λ (x) (process-arg x (+ qd-delta quote-depth))) (syntax->list stx))
+             (init-loc-wrapper #,cl #f #f #,quoted?))
+       #,(syntax-line stx) 
+       #,(syntax-column stx)
+       #,quoted?))
+  (syntax-case* stx (name unquote quote unquote-splicing term) (λ (x y) (eq? (syntax-e x) (syntax-e y)))
+    ['a (reader-shorthand #'a +1 (if (= quote-depth 0) "" "'"))]
+    [,a (reader-shorthand #'a -1 (if (= quote-depth 1) "" ","))]
+    [,@a (reader-shorthand #'a -1 (if (= quote-depth 1) "" ",@"))]
+    [(term a)
+     (if (= quote-depth 0)
+         #`(init-loc-wrapper 
+            (list (init-loc-wrapper "" #,(syntax-line stx) #,(syntax-column stx) #,quoted?)
+                  'spring
+                  #,(process-arg (cadr (syntax->list stx)) (+ quote-depth 1)))
+            #,(syntax-line stx) 
+            #,(syntax-column stx)
+            #,quoted?)
+         (handle-sequence +1))]
+    [(a ...)
+     (handle-sequence 0)]
+    [(a b ... . c)
+     #`(init-loc-wrapper 
+        (list (init-loc-wrapper #,op #,(syntax-line stx) #,(syntax-column stx) #,quoted?)
+              #,@(map (λ (x) (process-arg x quote-depth)) (syntax->list (syntax (a b ...))))
+              (init-loc-wrapper #," . " #f #f #,quoted?)
+              #,(process-arg #'c quote-depth)
+              (init-loc-wrapper #,cl #f #f #,quoted?))
+        #,(syntax-line stx) 
+        #,(syntax-column stx)
+        #,quoted?)]
+    [x 
+     (and (identifier? #'x)
+          (term-fn? (syntax-local-value #'x (λ () #f))))
+     #`(make-lw
+        '#,(syntax-e #'x)
+        #,(syntax-line stx) 
+        #f
+        #,(syntax-column stx)
+        #f
+        #f
+        #t)]
+    [x 
+     (identifier? #'x)
+     #`(init-loc-wrapper 
+        '#,(syntax-e #'x)
+        #,(syntax-line stx) 
+        #,(syntax-column stx)
+        #,quoted?)]
+    [x 
+     #`(init-loc-wrapper 
+        #,(let ([base (syntax-e #'x)])
+            (if (string? base)
+                #`(rewrite-quotes #,(format "~s" base))
+                (format "~s" (syntax-e #'x))))
+        #,(syntax-line stx) 
+        #,(syntax-column stx)
+        #,quoted?)]))
+
+(define (to-lw/proc stx)
+  (syntax-case stx ()
+    [(_ stx)
+     #`(add-spans #,(process-arg #'stx 1))]))
+(define (to-lw/uq/proc stx)
+  (syntax-case stx ()
+    [(_ stx)
+     #`(add-spans #,(process-arg #'stx 0))]))
\ No newline at end of file
diff --git a/collects/redex/private/loc-wrapper-rt.ss b/collects/redex/private/loc-wrapper-rt.ss
new file mode 100644
index 0000000000..b69474d6ab
--- /dev/null
+++ b/collects/redex/private/loc-wrapper-rt.ss
@@ -0,0 +1,96 @@
+#lang scheme/base
+
+;; this is the runtime code for loc-wrapper-ct.ss.
+;; it isn't really its own module, but separated
+;; out in order to get the phases right.
+(provide (all-defined-out))
+
+(require (lib "etc.ss")
+         "term.ss")
+
+(define (init-loc-wrapper e line column quoted?)
+  (make-lw e line #f column #f (not quoted?) #f))
+
+;; lw = (union 'spring loc-wrapper)
+
+;; e : (union string symbol #f (listof lw))
+;; line, line-span, column, column-span : number
+(define-struct lw (e line line-span column column-span unq? metafunction?) 
+  #:mutable
+  #:inspector (make-inspector))
+
+;; build-lw is designed for external consumption
+(define (build-lw e line line-span column column-span)
+  (make-lw e line line-span column column-span #f #f))
+
+(define curly-quotes-for-strings (make-parameter #t))
+
+(define (rewrite-quotes s)
+  (if (curly-quotes-for-strings)
+      (string-append "“"
+                     (substring s 1 (- (string-length s) 1))
+                     "”")
+      s))
+
+
+(define (add-spans lw)
+  (define line-seen-so-far 0)
+  
+  (define (add-spans/lw lw line col)
+    (cond
+      [(eq? lw 'spring) (values line col col)]
+      [else
+       (let ([start-line (or (lw-line lw) line line-seen-so-far)]
+             [start-column (or (lw-column lw) col 0)])
+         (set! line-seen-so-far (max line-seen-so-far start-line))
+         (unless (lw-line lw) (set-lw-line! lw line-seen-so-far))
+         (unless (lw-column lw) (set-lw-column! lw start-column))
+         (let-values ([(last-line first-column last-column)
+                       (add-spans/obj (lw-e lw) start-line start-column)])
+           (set-lw-line-span! lw (- last-line start-line))
+           (let ([new-col (min/f (lw-column lw)
+                                 first-column)])
+             (set-lw-column! lw new-col)
+             (set-lw-column-span! lw (- last-column new-col)))
+           (values last-line first-column last-column)))]))
+  (define (add-spans/obj e line col)
+    (cond
+      [(string? e) 
+       (values line col (+ col (string-length e)))]
+      [(symbol? e)
+       (values line col (+ col (string-length (symbol->string e))))]
+      [(not e) (values line col col)]
+      [else 
+       (let loop ([lws e]
+                  [line line]
+                  [first-column col]
+                  [last-column col]
+                  [current-col col])
+         (cond
+           [(null? lws) (values line first-column last-column)]
+           [else 
+            (let-values ([(last-line inner-first-column inner-last-column)
+                          (add-spans/lw (car lws) line current-col)])
+              (if (= last-line line)
+                  (loop (cdr lws)
+                        last-line
+                        (min inner-first-column first-column)
+                        (max inner-last-column last-column)
+                        inner-last-column)
+                  (loop (cdr lws)
+                        last-line
+                        (min inner-first-column first-column)
+                        inner-last-column
+                        inner-last-column)))]))]))
+  
+  (add-spans/lw lw #f #f)
+  lw)
+
+(define (min/f a b)
+  (cond
+    [(and a b) (min a b)]
+    [a a]
+    [b b]
+    [else 0]))
+
+
diff --git a/collects/redex/private/loc-wrapper.ss b/collects/redex/private/loc-wrapper.ss
index 4bc3b7df6f..666f3d8afa 100644
--- a/collects/redex/private/loc-wrapper.ss
+++ b/collects/redex/private/loc-wrapper.ss
@@ -1,181 +1,12 @@
 #lang scheme/base
 
-(require (lib "etc.ss")
-         "term.ss"
-         scheme/contract)
-(require (for-syntax "term-fn.ss" scheme/base))
+(require scheme/contract
+         (for-syntax scheme/base)
+         (for-syntax "loc-wrapper-ct.ss")
+         "loc-wrapper-rt.ss")
 
-(define (init-loc-wrapper e line column quoted?)
-  (make-lw e line #f column #f (not quoted?) #f))
-
-;; lw = (union 'spring loc-wrapper)
-
-;; e : (union string symbol #f (listof lw))
-;; line, line-span, column, column-span : number
-(define-struct lw (e line line-span column column-span unq? metafunction?) 
-  #:mutable
-  #:inspector (make-inspector))
-
-;; build-lw is designed for external consumption
-(define (build-lw e line line-span column column-span)
-  (make-lw e line line-span column column-span #f #f))
-
-(define curly-quotes-for-strings (make-parameter #t))
-
-(define (rewrite-quotes s)
-  (if (curly-quotes-for-strings)
-      (string-append "“"
-                     (substring s 1 (- (string-length s) 1))
-                     "”")
-      s))
-
-(define-syntax-set (to-lw to-lw/uq)
-  (define (process-arg stx quote-depth)
-    (define quoted? (quote-depth . > . 0))
-    (define-values (op cl)
-      (if (syntax? stx)
-          (case (syntax-property stx 'paren-shape)
-            [(#\{) (values "{" "}")]
-            [(#\[) (values "[" "]")]
-            [else (values "(" ")")])
-          (values #f #f)))
-    (define (reader-shorthand arg qd-delta mrk)
-      #`(init-loc-wrapper 
-         (list (init-loc-wrapper #,mrk
-                                 #,(syntax-line stx)
-                                 #,(syntax-column stx)
-                                 #,quoted?)
-               'spring
-               #,(process-arg arg (+ quote-depth qd-delta)))
-         #,(syntax-line stx) 
-         #,(syntax-column stx)
-         #,quoted?))
-    (define (handle-sequence qd-delta)
-      #`(init-loc-wrapper 
-         (list (init-loc-wrapper #,op #,(syntax-line stx) #,(syntax-column stx) #,quoted?)
-               #,@(map (λ (x) (process-arg x (+ qd-delta quote-depth))) (syntax->list stx))
-               (init-loc-wrapper #,cl #f #f #,quoted?))
-         #,(syntax-line stx) 
-         #,(syntax-column stx)
-         #,quoted?))
-    (syntax-case* stx (name unquote quote unquote-splicing term) (λ (x y) (eq? (syntax-e x) (syntax-e y)))
-      ['a (reader-shorthand #'a +1 (if (= quote-depth 0) "" "'"))]
-      [,a (reader-shorthand #'a -1 (if (= quote-depth 1) "" ","))]
-      [,@a (reader-shorthand #'a -1 (if (= quote-depth 1) "" ",@"))]
-      [(term a)
-       (if (= quote-depth 0)
-           #`(init-loc-wrapper 
-              (list (init-loc-wrapper "" #,(syntax-line stx) #,(syntax-column stx) #,quoted?)
-                    'spring
-                    #,(process-arg (cadr (syntax->list stx)) (+ quote-depth 1)))
-              #,(syntax-line stx) 
-              #,(syntax-column stx)
-              #,quoted?)
-           (handle-sequence +1))]
-      [(a ...)
-       (handle-sequence 0)]
-      [(a b ... . c)
-       #`(init-loc-wrapper 
-          (list (init-loc-wrapper #,op #,(syntax-line stx) #,(syntax-column stx) #,quoted?)
-                #,@(map (λ (x) (process-arg x quote-depth)) (syntax->list (syntax (a b ...))))
-                (init-loc-wrapper #," . " #f #f #,quoted?)
-                #,(process-arg #'c quote-depth)
-                (init-loc-wrapper #,cl #f #f #,quoted?))
-          #,(syntax-line stx) 
-          #,(syntax-column stx)
-          #,quoted?)]
-      [x 
-       (and (identifier? #'x)
-            (term-fn? (syntax-local-value #'x (λ () #f))))
-       #`(make-lw
-          '#,(syntax-e #'x)
-          #,(syntax-line stx) 
-          #f
-          #,(syntax-column stx)
-          #f
-          #f
-          #t)]
-      [x 
-       (identifier? #'x)
-       #`(init-loc-wrapper 
-          '#,(syntax-e #'x)
-          #,(syntax-line stx) 
-          #,(syntax-column stx)
-          #,quoted?)]
-      [x 
-       #`(init-loc-wrapper 
-          #,(let ([base (syntax-e #'x)])
-              (if (string? base)
-                  #`(rewrite-quotes #,(format "~s" base))
-                  (format "~s" (syntax-e #'x))))
-          #,(syntax-line stx) 
-          #,(syntax-column stx)
-          #,quoted?)]))
-  
-  (define (to-lw/proc stx)
-    (syntax-case stx ()
-      [(_ stx)
-       #`(add-spans #,(process-arg #'stx 1))]))
-  (define (to-lw/uq/proc stx)
-    (syntax-case stx ()
-      [(_ stx)
-       #`(add-spans #,(process-arg #'stx 0))])))
-
-(define (add-spans lw)
-  (define (add-spans/lw lw line col)
-    (cond
-      [(eq? lw 'spring) (values line col col)]
-      [else
-       (let ([start-line (or (lw-line lw) line)]
-             [start-column (or (lw-column lw) col)])
-         (when (and start-line  ;; if we don't have src loc info, just give up.
-                    start-column)
-           (let-values ([(last-line first-column last-column)
-                         (add-spans/obj (lw-e lw) start-line start-column)])
-             (unless (lw-line lw)
-               (set-lw-line! lw line))
-             (set-lw-line-span! lw (- last-line start-line))
-             
-             (unless (lw-column lw)
-               (set-lw-column! lw col))
-             (let ([new-col (min (lw-column lw)
-                                 first-column)])
-               (set-lw-column! lw new-col)
-               (set-lw-column-span! lw (- last-column new-col)))
-             
-             (values last-line first-column last-column))))]))
-  (define (add-spans/obj e line col)
-    (cond
-      [(string? e) 
-       (values line col (+ col (string-length e)))]
-      [(symbol? e)
-       (values line col (+ col (string-length (symbol->string e))))]
-      [(not e) (values line col col)]
-      [else 
-       (let loop ([lws e]
-                  [line line]
-                  [first-column col]
-                  [last-column col]
-                  [current-col col])
-         (cond
-           [(null? lws) (values line first-column last-column)]
-           [else 
-            (let-values ([(last-line inner-first-column inner-last-column)
-                          (add-spans/lw (car lws) line current-col)])
-              (if (= last-line line)
-                  (loop (cdr lws)
-                        last-line
-                        (min inner-first-column first-column)
-                        (max inner-last-column last-column)
-                        inner-last-column)
-                  (loop (cdr lws)
-                        last-line
-                        (min inner-first-column first-column)
-                        inner-last-column
-                        inner-last-column)))]))]))
-  
-  (add-spans/lw lw #f #f)
-  lw)
+(define-syntax (to-lw stx) (to-lw/proc stx))
+(define-syntax (to-lw/uq stx) (to-lw/uq/proc stx))
 
 (define pnum (and/c number? (or/c zero? positive?)))
 
diff --git a/collects/redex/private/pict.ss b/collects/redex/private/pict.ss
index 9a97ceac3a..ba4c88a0a3 100644
--- a/collects/redex/private/pict.ss
+++ b/collects/redex/private/pict.ss
@@ -580,9 +580,10 @@
                              [column (+ (lw-column fst)
                                         (lw-column-span fst))]
                              [column-span
-                              (- (lw-column snd)
-                                 (+ (lw-column fst)
-                                    (lw-column-span fst)))])
+                              (max (- (lw-column snd)
+                                      (+ (lw-column fst)
+                                         (lw-column-span fst)))
+                                   0)])
                         (build-lw (make-bar) line line-span column column-span))]
                      [else
                       (build-lw
diff --git a/collects/redex/private/reduction-semantics.ss b/collects/redex/private/reduction-semantics.ss
index b571764bbc..cddc9c5795 100644
--- a/collects/redex/private/reduction-semantics.ss
+++ b/collects/redex/private/reduction-semantics.ss
@@ -20,6 +20,46 @@
 (define (language-nts lang)
   (hash-map (compiled-lang-ht lang) (λ (x y) x)))
 
+#;
+(define-for-syntax (prune-syntax stx)
+  (datum->syntax
+   (identifier-prune-lexical-context #'whatever '())
+   (let loop ([stx stx])
+     (syntax-case stx (quote)
+       [(quote x) (list (quote-syntax/prune quote)
+                        (syntax->datum #'x))]
+       [x
+        (cond 
+          [(identifier? stx) (identifier-prune-lexical-context stx)] 
+          [(syntax? stx)
+           (datum->syntax (identifier-prune-lexical-context 
+                           #'whatever 
+                           '(#%app))
+                          (syntax-e stx)
+                          stx)]
+          [(pair? stx)
+           (cons (loop (car stx))
+                 (loop (cdr stx)))]
+          [else stx])]))))
+
+(define-for-syntax (prune-syntax stx)
+  stx
+  
+  #;
+  (datum->syntax
+   (identifier-prune-lexical-context #'whatever '(#%app #%datum))
+   (let loop ([stx stx])
+     (syntax-case stx (quote)
+       [(quote x) (list (quote-syntax/prune quote)
+                        (syntax->datum #'x))]
+       [(a . b) (cons (loop #'a) (loop #'b))]
+       [x 
+        (identifier? #'x)
+        (datum->syntax (identifier-prune-lexical-context #'x)
+                       (syntax-e #'x))]
+       [() '()]
+       [_ (syntax->datum stx)]))))
+
 (define-syntax (term-match/single stx)
   (syntax-case stx ()
     [(_ lang [pattern rhs] ...)
@@ -243,22 +283,23 @@
     (syntax-case stx ()
       [(_ id orig-reduction-relation allow-zero-rules? lang . w/domain-args)
        (identifier? #'lang)
-       (let-values ([(domain-pattern main-arrow args)
-                     (parse-keywords stx #'id #'w/domain-args)])
-         (with-syntax ([(rules ...) (before-with args)]
-                       [(shortcuts ...) (after-with args)])
-           (with-syntax ([(lws ...) (map rule->lws (syntax->list #'(rules ...)))])
-             (reduction-relation/helper 
-              stx
-              (syntax-e #'id)
-              #'orig-reduction-relation
-              (syntax lang)
-              (syntax->list (syntax (rules ...)))
-              (syntax->list (syntax (shortcuts ...)))
-              #'(list lws ...)
-              (syntax-e #'allow-zero-rules?)
-              domain-pattern
-              main-arrow))))]
+       (prune-syntax
+        (let-values ([(domain-pattern main-arrow args)
+                      (parse-keywords stx #'id #'w/domain-args)])
+          (with-syntax ([(rules ...) (before-with args)]
+                        [(shortcuts ...) (after-with args)])
+            (with-syntax ([(lws ...) (map rule->lws (syntax->list #'(rules ...)))])
+              (reduction-relation/helper 
+               stx
+               (syntax-e #'id)
+               #'orig-reduction-relation
+               (syntax lang)
+               (syntax->list (syntax (rules ...)))
+               (syntax->list (syntax (shortcuts ...)))
+               #'(list lws ...)
+               (syntax-e #'allow-zero-rules?)
+               domain-pattern
+               main-arrow)))))]
       [(_ id orig-reduction-relation allow-zero-rules? lang args ...)
        (raise-syntax-error (syntax-e #'id) 
                            "expected an identifier for the language name"
@@ -983,146 +1024,147 @@
            (raise-syntax-error syn-error-name "expected an identifier in the language position" orig-stx #'lang))
          (when (null? (syntax-e #'rest))
            (raise-syntax-error syn-error-name "no clauses" orig-stx))
-         (let-values ([(contract-name dom-ctcs codom-contract pats)
-                       (split-out-contract orig-stx syn-error-name #'rest)])
-           (with-syntax ([(((original-names lhs-clauses ...) rhs stuff ...) ...) pats]
-                         [(lhs-for-lw ...)
-                          (with-syntax ([((lhs-for-lw _ _ ...) ...) pats])
-                            (map (λ (x) (datum->syntax #f (cdr (syntax-e x)) x))
-                                 (syntax->list #'(lhs-for-lw ...))))])
-             (with-syntax ([(lhs ...) #'((lhs-clauses ...) ...)]
-                           [name (let loop ([name (if contract-name
-                                                      contract-name
-                                                      (car (syntax->list #'(original-names ...))))]
-                                            [names (if contract-name
-                                                       (syntax->list #'(original-names ...))
-                                                       (cdr (syntax->list #'(original-names ...))))])
-                                   (cond
-                                     [(null? names) name]
-                                     [else
-                                      (unless (eq? (syntax-e name) (syntax-e (car names)))
-                                        (raise
-                                         (make-exn:fail:syntax
-                                          (if contract-name
-                                              "define-metafunction: expected each clause and the contract to use the same name"
-                                              "define-metafunction: expected each clause to use the same name")
-                                          (current-continuation-marks)
-                                          (list name
-                                                (car names)))))
-                                      (loop name (cdr names))]))])
-               
-               (with-syntax ([(((tl-side-conds ...) ...) 
-                               (tl-bindings ...)
-                               (tl-side-cond/binds ...))
-                              (parse-extras #'((stuff ...) ...))])
-                 (let ([lang-nts (language-id-nts #'lang 'define-metafunction)])
-                   (with-syntax ([(tl-withs ...) (map (λ (sc/b) (bind-withs syn-error-name '() sc/b #t))
-                                                      (syntax->list #'(tl-side-cond/binds ...)))])
-                         (with-syntax ([(side-conditions-rewritten ...) 
-                                        (map (λ (x) (rewrite-side-conditions/check-errs
-                                                     lang-nts
-                                                     'define-metafunction
-                                                     #t
-                                                     x))
-                                             (syntax->list (syntax ((side-condition lhs tl-withs) ...))))]
-                                       [dom-side-conditions-rewritten
-                                        (and dom-ctcs
-                                             (rewrite-side-conditions/check-errs
-                                              lang-nts
-                                              'define-metafunction
-                                              #f
-                                              dom-ctcs))]
-                                       [codom-side-conditions-rewritten
-                                        (rewrite-side-conditions/check-errs
-                                         lang-nts
-                                         'define-metafunction
-                                         #f
-                                         codom-contract)]
-                                       [(rhs-fns ...)
-                                        (map (λ (lhs rhs bindings)
-                                               (let-values ([(names names/ellipses) (extract-names lang-nts 'define-metafunction #t lhs)])
-                                                 (with-syntax ([(names ...) names]
-                                                               [(names/ellipses ...) names/ellipses]
-                                                               [rhs rhs]
-                                                               [((tl-var tl-exp) ...) bindings])
-                                                   (syntax 
-                                                    (λ (name bindings)
-                                                      (term-let-fn ((name name))
-                                                                   (term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
-                                                                             (term-let ([tl-var (term tl-exp)] ...)
-                                                                                       (term rhs)))))))))
-                                             (syntax->list (syntax (lhs ...)))
-                                             (syntax->list (syntax (rhs ...)))
-                                             (syntax->list (syntax (tl-bindings ...))))]
-                                       [(name2 name-predicate) (generate-temporaries (syntax (name name)))]
-                                       [((side-cond ...) ...)
-                                        ;; For generating a pict, separate out side conditions wrapping the LHS and at the top-level
-                                        (map (lambda (lhs scs)
-                                               (append
-                                                (let loop ([lhs lhs])
-                                                  (syntax-case lhs (side-condition term)
-                                                    [(side-condition pat (term sc))
-                                                     (cons #'sc (loop #'pat))]
-                                                    [_else null]))
-                                                scs))
-                                             (syntax->list #'(lhs ...))
-                                             (syntax->list #'((tl-side-conds ...) ...)))]
-                                       [(((bind-id . bind-pat) ...) ...)
-                                        ;; Also for pict, extract pattern bindings
-                                        (map extract-pattern-binds (syntax->list #'(lhs ...)))]
-                                       [(((rhs-bind-id . rhs-bind-pat) ...) ...)
-                                        ;; Also for pict, extract pattern bindings
-                                        (map extract-term-let-binds (syntax->list #'(rhs ...)))]
-                                       [(((where-id where-pat) ...) ...)
-                                        ;; Also for pict, extract where bindings
-                                        #'(tl-bindings ...)])
-                           (syntax-property
-                            #`(begin
-                                (define-values (name2 name-predicate)
-                                  (let ([sc `(side-conditions-rewritten ...)]
-                                        [dsc `dom-side-conditions-rewritten])
-                                    (build-metafunction 
+         (prune-syntax
+          (let-values ([(contract-name dom-ctcs codom-contract pats)
+                        (split-out-contract orig-stx syn-error-name #'rest)])
+            (with-syntax ([(((original-names lhs-clauses ...) rhs stuff ...) ...) pats]
+                          [(lhs-for-lw ...)
+                           (with-syntax ([((lhs-for-lw _ _ ...) ...) pats])
+                             (map (λ (x) (datum->syntax #f (cdr (syntax-e x)) x))
+                                  (syntax->list #'(lhs-for-lw ...))))])
+              (with-syntax ([(lhs ...) #'((lhs-clauses ...) ...)]
+                            [name (let loop ([name (if contract-name
+                                                       contract-name
+                                                       (car (syntax->list #'(original-names ...))))]
+                                             [names (if contract-name
+                                                        (syntax->list #'(original-names ...))
+                                                        (cdr (syntax->list #'(original-names ...))))])
+                                    (cond
+                                      [(null? names) name]
+                                      [else
+                                       (unless (eq? (syntax-e name) (syntax-e (car names)))
+                                         (raise
+                                          (make-exn:fail:syntax
+                                           (if contract-name
+                                               "define-metafunction: expected each clause and the contract to use the same name"
+                                               "define-metafunction: expected each clause to use the same name")
+                                           (current-continuation-marks)
+                                           (list name
+                                                 (car names)))))
+                                       (loop name (cdr names))]))])
+                
+                (with-syntax ([(((tl-side-conds ...) ...) 
+                                (tl-bindings ...)
+                                (tl-side-cond/binds ...))
+                               (parse-extras #'((stuff ...) ...))])
+                  (let ([lang-nts (language-id-nts #'lang 'define-metafunction)])
+                    (with-syntax ([(tl-withs ...) (map (λ (sc/b) (bind-withs syn-error-name '() sc/b #t))
+                                                       (syntax->list #'(tl-side-cond/binds ...)))])
+                      (with-syntax ([(side-conditions-rewritten ...) 
+                                     (map (λ (x) (rewrite-side-conditions/check-errs
+                                                  lang-nts
+                                                  'define-metafunction
+                                                  #t
+                                                  x))
+                                          (syntax->list (syntax ((side-condition lhs tl-withs) ...))))]
+                                    [dom-side-conditions-rewritten
+                                     (and dom-ctcs
+                                          (rewrite-side-conditions/check-errs
+                                           lang-nts
+                                           'define-metafunction
+                                           #f
+                                           dom-ctcs))]
+                                    [codom-side-conditions-rewritten
+                                     (rewrite-side-conditions/check-errs
+                                      lang-nts
+                                      'define-metafunction
+                                      #f
+                                      codom-contract)]
+                                    [(rhs-fns ...)
+                                     (map (λ (lhs rhs bindings)
+                                            (let-values ([(names names/ellipses) (extract-names lang-nts 'define-metafunction #t lhs)])
+                                              (with-syntax ([(names ...) names]
+                                                            [(names/ellipses ...) names/ellipses]
+                                                            [rhs rhs]
+                                                            [((tl-var tl-exp) ...) bindings])
+                                                (syntax 
+                                                 (λ (name bindings)
+                                                   (term-let-fn ((name name))
+                                                                (term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
+                                                                          (term-let ([tl-var (term tl-exp)] ...)
+                                                                                    (term rhs)))))))))
+                                          (syntax->list (syntax (lhs ...)))
+                                          (syntax->list (syntax (rhs ...)))
+                                          (syntax->list (syntax (tl-bindings ...))))]
+                                    [(name2 name-predicate) (generate-temporaries (syntax (name name)))]
+                                    [((side-cond ...) ...)
+                                     ;; For generating a pict, separate out side conditions wrapping the LHS and at the top-level
+                                     (map (lambda (lhs scs)
+                                            (append
+                                             (let loop ([lhs lhs])
+                                               (syntax-case lhs (side-condition term)
+                                                 [(side-condition pat (term sc))
+                                                  (cons #'sc (loop #'pat))]
+                                                 [_else null]))
+                                             scs))
+                                          (syntax->list #'(lhs ...))
+                                          (syntax->list #'((tl-side-conds ...) ...)))]
+                                    [(((bind-id . bind-pat) ...) ...)
+                                     ;; Also for pict, extract pattern bindings
+                                     (map extract-pattern-binds (syntax->list #'(lhs ...)))]
+                                    [(((rhs-bind-id . rhs-bind-pat) ...) ...)
+                                     ;; Also for pict, extract pattern bindings
+                                     (map extract-term-let-binds (syntax->list #'(rhs ...)))]
+                                    [(((where-id where-pat) ...) ...)
+                                     ;; Also for pict, extract where bindings
+                                     #'(tl-bindings ...)])
+                        (syntax-property
+                         #`(begin
+                             (define-values (name2 name-predicate)
+                               (let ([sc `(side-conditions-rewritten ...)]
+                                     [dsc `dom-side-conditions-rewritten])
+                                 (build-metafunction 
+                                  lang
+                                  sc
+                                  (list rhs-fns ...)
+                                  #,(if prev-metafunction
+                                        (let ([term-fn (syntax-local-value prev-metafunction)])
+                                          #`(metafunc-proc-cps #,(term-fn-get-id term-fn)))
+                                        #''())
+                                  #,(if prev-metafunction
+                                        (let ([term-fn (syntax-local-value prev-metafunction)])
+                                          #`(metafunc-proc-rhss #,(term-fn-get-id term-fn)))
+                                        #''())
+                                  (λ (f/dom cps rhss)
+                                    (make-metafunc-proc
+                                     (let ([name (lambda (x) (f/dom x))]) name)
+                                     (list (list (to-lw lhs-for-lw)
+                                                 (list (to-lw/uq side-cond) ...)
+                                                 (list (cons (to-lw bind-id)
+                                                             (to-lw bind-pat))
+                                                       ...
+                                                       (cons (to-lw rhs-bind-id)
+                                                             (to-lw/uq rhs-bind-pat))
+                                                       ...
+                                                       (cons (to-lw where-id)
+                                                             (to-lw where-pat))
+                                                       ...)
+                                                 (to-lw rhs))
+                                           ...)
                                      lang
-                                     sc
-                                     (list rhs-fns ...)
-                                     #,(if prev-metafunction
-                                           (let ([term-fn (syntax-local-value prev-metafunction)])
-                                             #`(metafunc-proc-cps #,(term-fn-get-id term-fn)))
-                                           #''())
-                                     #,(if prev-metafunction
-                                           (let ([term-fn (syntax-local-value prev-metafunction)])
-                                             #`(metafunc-proc-rhss #,(term-fn-get-id term-fn)))
-                                           #''())
-                                     (λ (f/dom cps rhss)
-                                       (make-metafunc-proc
-                                        (let ([name (lambda (x) (f/dom x))]) name)
-                                        (list (list (to-lw lhs-for-lw)
-                                                    (list (to-lw/uq side-cond) ...)
-                                                    (list (cons (to-lw bind-id)
-                                                                (to-lw bind-pat))
-                                                          ...
-                                                          (cons (to-lw rhs-bind-id)
-                                                                (to-lw/uq rhs-bind-pat))
-                                                          ...
-                                                          (cons (to-lw where-id)
-                                                                (to-lw where-pat))
-                                                          ...)
-                                                    (to-lw rhs))
-                                              ...)
-                                        lang
-                                        #t ;; multi-args?
-                                        'name
-                                        cps
-                                        rhss
-                                        (let ([name (lambda (x) (name-predicate x))]) name)
-                                        dsc
-                                        sc))
+                                     #t ;; multi-args?
+                                     'name
+                                     cps
+                                     rhss
+                                     (let ([name (lambda (x) (name-predicate x))]) name)
                                      dsc
-                                     `codom-side-conditions-rewritten
-                                     'name)))
-                                (term-define-fn name name2))
-                            'disappeared-use
-                            (map syntax-local-introduce (syntax->list #'(original-names ...))))))))))))]
+                                     sc))
+                                  dsc
+                                  `codom-side-conditions-rewritten
+                                  'name)))
+                             (term-define-fn name name2))
+                         'disappeared-use
+                         (map syntax-local-introduce (syntax->list #'(original-names ...)))))))))))))]
       [(_ prev-metafunction name lang clauses ...)
        (begin
          (unless (identifier? #'name)
@@ -1361,23 +1403,24 @@
      (identifier? (syntax name))
      (begin
        (check-rhss-not-empty stx (cddr (syntax->list stx)))
-       (with-syntax ([((nt-names orig) ...) (pull-out-names 'define-language stx #'(names ...))])
-         (with-syntax ([(subst-names ...) (generate-temporaries (syntax->list #'(nt-names ...)))])
-           (syntax/loc stx
-             (begin
-               (define-syntax name
-                 (make-set!-transformer
-                  (make-language-id
-                   (case-lambda
-                     [(stx)
-                      (syntax-case stx (set!)
-                        [(set! x e) (raise-syntax-error 'define-language "cannot set! identifier" stx #'e)]
-                        [(x e (... ...)) #'(define-language-name e (... ...))]
-                        [x 
-                         (identifier? #'x)
-                         #'define-language-name])])
-                   '(nt-names ...))))
-               (define define-language-name (language name (names rhs ...) ...)))))))]))
+       (prune-syntax
+        (with-syntax ([((nt-names orig) ...) (pull-out-names 'define-language stx #'(names ...))])
+          (with-syntax ([(subst-names ...) (generate-temporaries (syntax->list #'(nt-names ...)))])
+            (syntax/loc stx
+              (begin
+                (define-syntax name
+                  (make-set!-transformer
+                   (make-language-id
+                    (case-lambda
+                      [(stx)
+                       (syntax-case stx (set!)
+                         [(set! x e) (raise-syntax-error 'define-language "cannot set! identifier" stx #'e)]
+                         [(x e (... ...)) #'(define-language-name e (... ...))]
+                         [x 
+                          (identifier? #'x)
+                          #'define-language-name])])
+                    '(nt-names ...))))
+                (define define-language-name (language name (names rhs ...) ...))))))))]))
 
 (define-struct binds (source binds))