diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt
index 80f5c02244..2042fad40a 100644
--- a/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt
+++ b/pkgs/redex-pkgs/redex-lib/redex/private/enum.rkt
@@ -1,11 +1,13 @@
 #lang racket/base
 (require racket/contract
+         racket/function
          racket/list
          racket/match
-         racket/function
+         racket/set
+
+         "enumerator.rkt"
          "lang-struct.rkt"
          "match-a-pattern.rkt"
-         "enumerator.rkt"
          "recursive-lang.rkt")
 
 (provide 
@@ -18,7 +20,7 @@
   [lang-enum? (-> any/c boolean?)]
   [enum? (-> any/c boolean?)]))
 
-(struct lang-enum (enums))
+(struct lang-enum (enums unused-var/e))
 (struct repeat (n terms) #:transparent)
 (struct decomposition (ctx term) #:transparent)
 (struct named (name val) #:transparent)
@@ -36,6 +38,9 @@
 
 (define (lang-enumerators lang)
   (define l-enums (make-hash))
+  (define unused-var/e
+    (except/e var/e
+              (used-vars lang)))
   (define (enumerate-lang cur-lang enum-f)
     (for-each
      (λ (nt)
@@ -50,14 +55,15 @@
                  (map ((curry map-nt-rhs-pat) name-all-repeats)
                       lang))])
     (enumerate-lang fin-lang
-                    enumerate-rhss)
+                    (λ (rhs enums)
+                       (enumerate-rhss rhs enums unused-var/e)))
     (enumerate-lang rec-lang
                     (λ (rhs enums)
                        (thunk/e +inf.f
-                                   (λ ()
-                                      (enumerate-rhss rhs enums)))))
+                                (λ ()
+                                   (enumerate-rhss rhs enums unused-var/e)))))
 
-    (lang-enum l-enums)))
+    (lang-enum l-enums unused-var/e)))
 
 (define (pat-enumerator l-enum pat)
   (map/e
@@ -65,20 +71,23 @@
    (λ (_)
       (error 'pat-enum "Enumerator is not a  bijection"))
    (pat/e pat
-             (lang-enum-enums l-enum))))
+          (lang-enum-enums l-enum)
+          (lang-enum-unused-var/e l-enum))))
 
-(define (enumerate-rhss rhss l-enums)
+(define (enumerate-rhss rhss l-enums unused/e)
   (apply sum/e
          (map
           (λ (rhs)
              (pat/e (rhs-pattern rhs)
-                       l-enums))
+                    l-enums
+                    unused/e))
           rhss)))
 
-(define (pat/e pat l-enums)
+(define (pat/e pat l-enums unused/e)
   (enum-names pat
               (sep-names pat)
-              l-enums))
+              l-enums
+              unused/e))
 
 (define (map-nt-rhs-pat f nonterminal)
   (nt (nt-name nonterminal)
@@ -278,11 +287,11 @@
                             n)))
              (assoc-named n (cdr l)))]))
 
-(define (enum-names pat nps nt-enums)
+(define (enum-names pat nps nt-enums unused-var/e)
   (let rec ([nps nps]
             [env (hash)])
     (cond [(empty-named-pats? nps)
-           (pat/e-with-names pat nt-enums env)]
+           (pat/e-with-names pat nt-enums env unused-var/e)]
           [else
            (let ([cur (next-named-pats nps)])
              (cond [(named? cur)
@@ -304,7 +313,7 @@
                                      name
                                      (named-name n))))
                        (dep/e
-                        (pat/e-with-names pat nt-enums env)
+                        (pat/e-with-names pat nt-enums env unused-var/e)
                         (λ (term)
                            (rec (rest-named-pats nps)
                                 (hash-set env
@@ -332,10 +341,11 @@
                          (λ (excepts pat)
                             (except/e
                              (pat/e-with-names pat
-                                                  nt-enums
-                                                  (hash-set env
-                                                            (mismatch-name cur)
-                                                            excepts))
+                                               nt-enums
+                                               (hash-set env
+                                                         (mismatch-name cur)
+                                                         excepts)
+                                               unused-var/e)
                              excepts))
                          (mismatch-val cur))
                         (λ (terms)
@@ -345,7 +355,7 @@
                                           terms))))))]
                    [else (error 'unexpected "expected name, mismatch or unimplemented, got: ~a in ~a" cur nps)]))])))
 
-(define (pat/e-with-names pat nt-enums named-terms)
+(define (pat/e-with-names pat nt-enums named-terms unused-var/e)
   (let loop ([pat pat])
     (match-a-pattern
      pat
@@ -366,7 +376,7 @@
       ;; todo
       (error 'unimplemented "var-prefix")]
      [`variable-not-otherwise-mentioned
-      (error 'unimplemented "var-not-mentioned")] ;; error
+      unused-var/e]
      [`hole
       (const/e the-hole)]
      [`(nt ,id)
@@ -452,20 +462,25 @@
    (listof/e char/e)))
 
 (define integer/e
+  #; ;; Simple "turn down the volume" list
+  (from-list/e '(0 1 -1))
   (sum/e nats
-            (map/e (λ (n) (- (+ n 1)))
-                      (λ (n) (- (- n) 1))
-                      nats)))
+         (map/e (λ (n) (- (+ n 1)))
+                (λ (n) (- (- n) 1))
+                nats)))
 
-(define real/e (from-list/e '(0.5 1.5 123.112354)))
+;; This is really annoying so I turned it off
+(define real/e empty/e)
 (define num/e
   (sum/e integer/e
-            real/e))
+         real/e))
 
 (define bool/e
   (from-list/e '(#t #f)))
 
 (define var/e
+  #; ;; "turn down the volume" variables
+  (from-list/e '(x y z))
   (map/e
    (compose string->symbol list->string list)
    (compose car string->list symbol->string)
@@ -473,9 +488,9 @@
 
 (define any/e
   (sum/e num/e
-            string/e
-            bool/e
-            var/e))
+         string/e
+         bool/e
+         var/e))
 
 (define (to-term aug)
   (cond [(named? aug)
diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/recursive-lang.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/recursive-lang.rkt
index a5aa4dae3b..ee719e2861 100644
--- a/pkgs/redex-pkgs/redex-lib/redex/private/recursive-lang.rkt
+++ b/pkgs/redex-pkgs/redex-lib/redex/private/recursive-lang.rkt
@@ -10,7 +10,9 @@
  (contract-out
   [sep-lang (-> (listof nt?)
                 (values (listof nt?)
-                        (listof nt?)))]))
+                        (listof nt?)))]
+  [used-vars (-> (listof nt?)
+                 (listof symbol?))]))
 
 ;; sep-lang : lang -> lang lang
 ;; topologically sorts non-terminals by dependency
@@ -198,6 +200,52 @@
                                  (cdr (assoc r2 rec-nts))))))))
      lang)))
 
+;; used-vars : lang -> (listof symbol)
+(define (used-vars lang)
+  (set->list
+   (fold-map/set
+    (λ (the-nt)
+       (fold-map/set
+        (λ (the-rhs)
+           (let loop ([pat (rhs-pattern the-rhs)])
+             (match-a-pattern
+              pat
+              [`any (set)]
+              [`number (set)]
+              [`string (set)]
+              [`natural (set)]
+              [`integer (set)]
+              [`real (set)]
+              [`boolean (set)]
+              [`variable (set)]
+              [`(variable-except ,s ...) (set)]
+              [`(variable-prefix ,s) (set)]
+              [`variable-not-otherwise-mentioned (set)]
+              [`hole (set)]
+              ;; Not sure
+              [`(nt ,id) (set)]
+              [`(name ,name ,pat) (set)]
+              [`(mismatch-name ,name ,pat) (set)]
+              [`(in-hole ,p1 ,p2)
+               (set-union (loop p1)
+                          (loop p2))]
+              [`(hide-hole ,p) (loop p)]
+              ;; not sure about these 2, but they are unsupported by enum anyway
+              [`(side-condition ,p ,g ,e) (set)] 
+              [`(cross ,s) (set)]
+              [`(list ,sub-pats ...)
+               (fold-map/set
+                (λ (sub-pat)
+                   (match sub-pat
+                     [`(repeat ,pat ,name ,mismatch)
+                      (loop pat)]
+                     [else (loop sub-pat)]))
+                sub-pats)]
+              [(? (compose not pair?))
+               (set pat)])))
+        (nt-rhs the-nt)))
+    lang)))
+
 ;; fold-map/set : (a -> setof b) (listof a) -> (setof b)
 (define (fold-map/set f l)
   (foldl
diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/enum-test.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/enum-test.rkt
index 4215142e03..2ff840840f 100644
--- a/pkgs/redex-pkgs/redex-test/redex/tests/enum-test.rkt
+++ b/pkgs/redex-pkgs/redex-test/redex/tests/enum-test.rkt
@@ -77,3 +77,10 @@
 (try-it 100 M m)
 (try-it 100 M n)
 (try-it 100 M p)
+
+;; test variable-not-otherwise-mentioned
+(define-language VarMentioned
+  (mention a b c x y z)
+  (var variable-not-otherwise-mentioned))
+
+(try-it 20 VarMentioned var)