diff --git a/collects/redex/private/jdg-gen.rkt b/collects/redex/private/jdg-gen.rkt
index 5e14bac56e..1dc9b93d25 100644
--- a/collects/redex/private/jdg-gen.rkt
+++ b/collects/redex/private/jdg-gen.rkt
@@ -32,9 +32,12 @@
       (let recur ([p p])
         (match p
           [(lvar id)
-           (recur (hash-ref eqs p))]
+           ;; careful! term-e has terms, eqs has pats!
+           (hash-ref term-e p
+              (λ () (recur (hash-ref eqs p))))]
           [`(name ,id ,(bound))
-           (recur (hash-ref eqs (lvar id)))]
+           (hash-ref term-e (lvar id)
+              (λ () (recur (hash-ref eqs (lvar id)))))]
           [`(list ,ps ...)
            `(,@(for/list ([p ps]) (recur p)))]
           [`(cstr (,nts ...) ,p)
@@ -61,16 +64,16 @@
            [`(nt ,p-nt)
             (define all-nts (cons p-nt nts))
             (for/not-failed ([nt-pat all-nts])
-              (define term (recur `(nt ,nt-pat)))
-              (and/fail (for/and ([nt (remove nt-pat all-nts)])
-                          ((get-matcher nt) term))
-                        term))]
+                            (define term (recur `(nt ,nt-pat)))
+                            (and/fail (for/and ([nt (remove nt-pat all-nts)])
+                                        ((get-matcher nt) term))
+                                      term))]
            [`any
             (for/not-failed ([nt-pat nts])
-              (define term (recur `(nt ,nt-pat)))
-              (and/fail (for/and ([nt (remove nt-pat nts)])
-                          ((get-matcher nt) term))
-                        term))]
+                            (define term (recur `(nt ,nt-pat)))
+                            (and/fail (for/and ([nt (remove nt-pat nts)])
+                                        ((get-matcher nt) term))
+                                      term))]
            [_
             (define term (recur pat))
             (and/fail (for/and ([nt nts])
diff --git a/collects/redex/private/pat-unify.rkt b/collects/redex/private/pat-unify.rkt
index de4d0b5a9a..5452b4d16d 100644
--- a/collects/redex/private/pat-unify.rkt
+++ b/collects/redex/private/pat-unify.rkt
@@ -151,6 +151,7 @@
 ;; disqequations generated (by mismatch-pattern) during a given unification pass
 (define dqs-found (make-parameter (make-hash)))
 
+
 ;; pat pat env -> (or/c p*e #f)
 (define (unify t u e L)
   (parameterize ([dqs-found (make-hash)])
@@ -161,20 +162,22 @@
                           (not-failed? u*)
                           (unify* t* u* eqs L)))
     (and/fail (not-failed? res)
-         (let* ([static-eqs (hash/mut->imm eqs)]
-                [found-pre-dqs 
-                 (apply set-union (set) 
-                        (for/list ([dq-sides/id (hash-values (dqs-found))])
-                          (list->dq-pairs dq-sides/id)))]
-                [found-dqs
-                 (for/list ([pdq found-pre-dqs])
-                   (disunify* '() (first pdq) (second pdq) (hash-copy static-eqs) L))])
-           (and/fail (for/and ([d found-dqs]) d)
-                     (let* ([real-dqs (filter (λ (dq) (not (boolean? dq))) found-dqs)]
-                            [new-dqs (check-and-resimplify static-eqs (append real-dqs (env-dqs e)) L)])
-                       (and/fail new-dqs
-                                 (p*e res
-                                      (env static-eqs new-dqs)))))))))
+              (let* ([static-eqs (hash/mut->imm (let ([ans eqs])
+                                                  ;(printf "1.1\n")
+                                                  ans))]
+                     [found-pre-dqs 
+                      (apply set-union (set) 
+                             (for/list ([dq-sides/id (hash-values (dqs-found))])
+                               (list->dq-pairs dq-sides/id)))]
+                     [found-dqs
+                      (for/list ([pdq found-pre-dqs])
+                        (disunify* '() (first pdq) (second pdq) (hash-copy static-eqs) L))])
+                (and/fail (for/and ([d found-dqs]) d)
+                          (let* ([real-dqs (filter (λ (dq) (not (boolean? dq))) found-dqs)]
+                                 [new-dqs (check-and-resimplify static-eqs (append real-dqs (env-dqs e)) L)])
+                            (and/fail new-dqs
+                                      (p*e res
+                                           (env static-eqs new-dqs)))))))))
 
 (define (list->dq-pairs dq-sides)
   (cond
@@ -186,6 +189,7 @@
                          (list (car dq-sides) rhs))
                 (list->dq-pairs (cdr dq-sides)))]))
 
+
 ;; pat pat env lang -> (or/c env #f)
 (define (disunify params t u e L)
   (parameterize ([new-eqs (make-hash)])
@@ -259,7 +263,7 @@
            
                 
 (define (hash/mut->imm h0)
-  (for/fold ([h (hash)])
+  (for/fold ([h (hash)]) 
     ([(k v) (in-hash h0)])
     (hash-set h k v)))                                    
                                            
@@ -397,11 +401,13 @@
      (unify* u t e L)]
     ;; cstrs
     [(`(cstr (,nts1 ...) ,p1) `(cstr (,nts2 ...) ,p2))
-     (let ([res (unify* p1 p2 e L)])
+     (let ([res (unify* p1 p2 e L)]
+           [new-nts (merge-ids/sorted nts1 nts2 L)])
        (and/fail (not-failed? res)
+                 new-nts
                  (when (lvar? res)
                    (error 'unify* "unify* returned lvar as result: ~s\n~s\n~s\n" p1 p2 e))
-                 `(cstr ,(merge-ids/sorted nts1 nts2) ,res)))]
+                 `(cstr ,new-nts ,res)))]
     [(`(cstr ,nts ,p) _)
      (let ([res (unify* p u e L)])
        (and/fail (not-failed? res)
@@ -409,12 +415,16 @@
                    [(lvar id)
                     (error 'unify* "unify* returned lvar as result: ~s\n~s\n~s\n" p u e)]
                    [`(nt ,nt)
-                    `(cstr ,(merge-ids/sorted (list nt) nts)
-                           ,p)]
+                    (define new-nts (merge-ids/sorted (list nt) nts L))
+                    (and/fail new-nts
+                              `(cstr ,new-nts ,p))]
                    [`(cstr ,nts2 ,new-p)
-                    `(cstr ,(merge-ids/sorted nts nts2) ,new-p)]
+                    (define new-nts (merge-ids/sorted nts nts2 L))
+                    (and/fail new-nts
+                              `(cstr ,new-nts ,new-p))]
                    [_
-                    `(cstr ,nts ,res)])))]
+                    (and/fail (for/and ([n nts]) (check-nt n L res))
+                              `(cstr ,nts ,res))])))]
     [(_ `(cstr ,nts ,p))
      (unify* `(cstr ,nts ,p) t e L)]
     ;; nts
@@ -423,13 +433,15 @@
          (hash-ref (compiled-lang-collapsible-nts L) n)
          `(nt ,n))]
     [(`(nt ,p) u)
-     (if (hash-has-key? (compiled-lang-collapsible-nts L) p)
-         (unify* (hash-ref (compiled-lang-collapsible-nts L) p) u e L)
-         (let ([res (unify* u u e L)])
-           (and/fail (not-failed? res)
-                     (when (lvar? res)
-                       (error 'unify* "unify* returned lvar as result: ~s\n~s\n~s\n" u u e))
-                     `(cstr (,p) ,res))))]
+     (and/fail
+      (check-nt p L u)
+      (if (hash-has-key? (compiled-lang-collapsible-nts L) p)
+          (unify* (hash-ref (compiled-lang-collapsible-nts L) p) u e L)
+          (let ([res (unify* u u e L)]) ;; look at structure of nt here?
+            (and/fail (not-failed? res)
+                      (when (lvar? res)
+                        (error 'unify* "unify* returned lvar as result: ~s\n~s\n~s\n" u u e))
+                      `(cstr (,p) ,res)))))]
     [(_ `(nt ,p))
      (unify* `(nt ,p) t e L)]
     ;; other pat stuff
@@ -610,8 +622,10 @@
     [(_ _)
      (equal? p* u*)]))
 
-(define (merge-ids/sorted l1 l2)
-  (de-dupe/sorted (merge/sorted l1 l2)))
+(define (merge-ids/sorted l1 l2 lang)
+  (and (for*/and ([nt1 l1] [nt2 l2])
+         (check-nt nt1 lang `(nt ,l2)))
+       (de-dupe/sorted (merge/sorted l1 l2))))
 
 (define (symbol<? s1 s2)
   (string<? (symbol->string s1) (symbol->string s2)))
@@ -672,3 +686,72 @@
     [_
      (values (lvar id) res)]))
 
+(provide check-nt)
+
+(define check-nt
+  (let ([memo (hash)])
+    (λ (nt clang pat)
+      (define npat (normalize-pat pat))
+      (hash-ref memo (list nt clang npat)
+                (λ ()
+                  (define pat-ok? 
+                    (for/or ([ntp (in-list (map normalize-pat (nt-pats nt clang)))])
+                      (not-failed? (unify* npat ntp #f empty-lang))))
+                  (set! memo
+                        (hash-set memo (list nt clang npat) pat-ok?)))))))
+
+(define (normalize-pat pat)
+  (let loop ([pat pat])
+    (match-a-pattern pat
+                     [`any pat]
+                     [`number pat]
+                     [`string pat]
+                     [`natural pat]
+                     [`integer pat]
+                     [`real pat]
+                     [`boolean pat]
+                     [`variable pat]
+                     [`(variable-except ,s ...) `variable]
+                     [`(variable-prefix ,s) `variable]
+                     [`variable-not-otherwise-mentioned pat]
+                     [`hole (error "can't normalize pattern: ~s" pat)]
+                     [`(nt ,id) `any]
+                     [`(name ,name ,npat)
+                      (if (bound? npat)
+                          `any
+                          `(name ,name ,(loop npat)))]
+                     [`(mismatch-name ,name ,pat) (loop pat)]
+                     [`(in-hole ,p1 ,p2) (error "can't normalize pattern: ~s" pat)]
+                     [`(hide-hole ,p) (loop p)]
+                     [`(side-condition ,p ,g ,e)
+                      (error "can't normalize pattern: ~s" pat)]
+                     [`(cross ,s) (error "can't normalize pattern: ~s" pat)]
+                     [`(list ,sub-pats ...)
+                      `(list ,@(for/list ([sub-pat (in-list sub-pats)])
+                                 (match sub-pat
+                                   [`(repeat ,pat ,name ,mismatch)
+                                    (error "can't normalize pattern: ~s" pat)]
+                                   [else
+                                    (loop sub-pat)])))]
+                     [(? (compose not pair?)) 
+                      pat])))
+
+(define (nt-pats nt lang)
+  (define this-rhs
+    (nt-rhs
+     (let ([the-nt (findf (λ (lang-nt)
+                        (equal? nt (nt-name lang-nt)))
+                      (compiled-lang-lang lang))])
+       (unless the-nt
+         (error 'unify "nonterminal ~s not found for provided language... nts found: ~s" 
+                nt (hash-keys (compiled-lang-nt-map lang))))
+       the-nt)))
+  (match this-rhs
+    [(list (rhs `(nt ,alias)))
+     (nt-pats alias lang)]
+    [_
+     (map rhs-pattern this-rhs)]))
+       
+(define empty-lang
+  (compiled-lang
+   #f #f #f #f #f #f #f #f #f #f '() #f (hash)))
diff --git a/collects/redex/private/search.rkt b/collects/redex/private/search.rkt
index 5a7fcb295b..6288a211d8 100644
--- a/collects/redex/private/search.rkt
+++ b/collects/redex/private/search.rkt
@@ -45,6 +45,12 @@
 
 (define-struct gen-trace (tr-loc clause input state bound env) #:prefab)
 
+
+(define bt-count (make-parameter 0))
+(define BT-LIMIT 40)
+(define (inc-bt-count) 
+  (bt-count (add1 (bt-count))))
+
 (define (search/next clauses input bound lang)
   (define name-nums 0)
   (define fresh-pat (parameterize ([unique-name-nums 0])
@@ -57,7 +63,7 @@
   (define v-locs (make-hash))
   (λ ()
     (parameterize ([unique-name-nums name-nums]
-                   [visited-locs v-locs])
+                   [bt-count 0])
       (define-values (ans fails)
         (with-handlers ([exn:fail:redex:search-failure? (λ (e) 
                                                           (define f-conts (exn:fail:redex:search-failure-fails e))
@@ -69,7 +75,6 @@
       (set-last-gen-trace! (generation-trace))
       (set! fs (shuffle-fails fails))  ;; how to test if we're randomizing here?
       (set! name-nums (unique-name-nums))
-      (set! v-locs (visited-locs))
       ans)))
   
 (define (trim-fails fs)
@@ -90,6 +95,7 @@
     [else fs]))
 
 (define (fail-back fs)
+  (inc-bt-count)
   (match fs
     [(list (fail-cont e f b) rest ...)
      (choose-rule e f rest)]
@@ -100,10 +106,7 @@
     [(empty? fringe)
      (values env fail)]
     [else
-     (define new-f fringe)
-     (if new-f
-         (push-down (car new-f) env (cdr new-f) fail)
-         (fail-back fail))]))
+     (push-down (car fringe) env (cdr fringe) fail)]))
 
 (define (push-down a-partial-rule env fringe fail)
   (match a-partial-rule
@@ -184,7 +187,6 @@
             ['() 
              (p*e (p*e-p head-p*e) e)]
             [(cons (eqn lhs rhs) rest)
-             (eqn lhs rhs)
              (define u-res (unify lhs rhs e lang))
              (and (not-failed? u-res)
                   (loop (p*e-e u-res) rest))]))]
@@ -236,38 +238,18 @@
                           [(prem mk-clauses pat)
                            (prem mk-clauses (fresh-pat-vars pat instantiations))]))]))
 
-(define visited-locs (make-parameter (make-hash)))
-
 (define-struct (exn:fail:redex:search-failure exn:fail:redex) (fails))
 
 (define (check-depth-limits bound tr-loc fails)
+  (when (> (bt-count) BT-LIMIT)
+    (define str (format "backtrack count of ~s exceeded at ~s" BT-LIMIT tr-loc))
+    (raise (make-exn:fail:redex:search-failure str (current-continuation-marks) fails)))
   (when (> (length tr-loc) (* 3 (+ (length tr-loc) bound)))
     (define str (format "depth bound exceeded at depth: ~s" (length tr-loc)))
     (raise (make-exn:fail:redex:search-failure str (current-continuation-marks) fails))))
 
-(define (check-backtrack-limits tr-loc)
-  (define v-locs (visited-locs))
-  (when (< 5 (hash-ref v-locs tr-loc 0))
-    (define str (format "backtracking limit exceeded at location: ~s" tr-loc))
-    (raise (make-exn:fail:redex:search-failure str (current-continuation-marks))))
-  (define loc-count (hash-ref v-locs tr-loc 0))
-  (for ([(k v) (in-hash v-locs)])
-    (let loop ([l1 tr-loc]
-               [l2 k])
-      (cond
-        [(null? l1)
-         (void)]
-        [(null? l2)
-         (hash-set! v-locs k 0)]
-        [(= (car l1) (car l2))
-         (loop (cdr l1) (cdr l2))]
-        [else
-         (void)])))
-  (hash-set! v-locs tr-loc (add1 (hash-ref v-locs tr-loc 0))))
-
 (define unique-name-nums (make-parameter 0))
 
-
 (define generation-logger (make-logger 'generation-log (current-logger)))
 
 (define gen-log-recv #f)
diff --git a/collects/redex/tests/unify-tests.rkt b/collects/redex/tests/unify-tests.rkt
index 37f54b9e30..27e335aff0 100644
--- a/collects/redex/tests/unify-tests.rkt
+++ b/collects/redex/tests/unify-tests.rkt
@@ -254,7 +254,22 @@
            res-p
            res-p-bkwd)]))
 
-(define-language L0)
+;; This looks really strange but it is for backwards compatability
+;; with tests that didn't take nonterminal productions into account.
+;; There nts will all (except n) accept anything, but since they
+;; have two productions they don't get collapsed (and so will create
+;; cstr's).
+(define-language L0
+  (e any any)
+  (q any any)
+  (v any any)
+  (b any any)
+  (x any any)
+  (Γ any any)
+  (s any any)
+  (a any any)
+  (Q any any)
+  (n number any))
 
 
 (check-equal? (unify/format `number `number (hash) L0)
@@ -540,7 +555,7 @@
   ['boolean `(name x ,(bound)) (make-hash `((,(lvar 'x) . boolean)))]
   ['variable `(name x ,(bound)) (make-hash `((,(lvar 'x) . variable)))]
   ['variable-not-otherwise-mentioned `(name x ,(bound)) (make-hash `((,(lvar 'x) . variable-not-otherwise-mentioned)))]
-  ['(cstr (number) any) `(name x ,(bound)) (make-hash `((,(lvar 'x) . (cstr (number) any))))]
+  ['(cstr (n) any) `(name x ,(bound)) (make-hash `((,(lvar 'x) . (cstr (n) any))))]
   ['(list 1 2) `(name x ,(bound)) (make-hash `((,(lvar 'x) . (list 1 2))))]
   ['(mismatch-name z any) `(name x ,(bound)) (make-hash `((,(lvar 'x) . any)))]
   ['(nt q) `(name x ,(bound)) (make-hash `((,(lvar 'x) . (cstr (q) any))))]))
@@ -555,7 +570,8 @@
   
   (define-language ntl
     (n number)
-    ((x y) variable))
+    ((x y) variable)
+    (Q any any))
   
   (check-equal? (unify/format `(nt n) `any (hash) ntl)
                 (p*e `number (hash)))