diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/fresh.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/fresh.rkt
index 353cacc199..257a6278c9 100644
--- a/pkgs/redex-pkgs/redex-lib/redex/private/fresh.rkt
+++ b/pkgs/redex-pkgs/redex-lib/redex/private/fresh.rkt
@@ -1,44 +1,46 @@
 #lang racket/base
-(require racket/contract)
+(require racket/contract
+         racket/set)
 
-(define re:gen-d #rx".*[^0-9]([0-9]+)$")
 (define (variable-not-in sexp var)
-  (let* ([var-str (symbol->string var)]
-         [var-prefix (let ([m (regexp-match #rx"^(.*[^0-9])[0-9]+$" var-str)])
-                       (if m
-                           (cadr m)
-                           var-str))]
-         [found-exact-var? #f]
-         [nums (let loop ([sexp sexp]
-                          [nums null])
-                 (cond
-                   [(pair? sexp) (loop (cdr sexp) (loop (car sexp) nums))]
-                   [(symbol? sexp) 
-                    (when (eq? sexp var)
-                      (set! found-exact-var? #t))
-                    (let* ([str (symbol->string sexp)]
-                           [match (regexp-match re:gen-d str)])
-                      (if (and match
-                               (is-prefix? var-prefix str))
-                          (cons (string->number (cadr match)) nums)
-                          nums))]
-                   [else nums]))])
-    (cond
-      [(not found-exact-var?) var]
-      [(null? nums) (string->symbol (format "~a1" var))]
-      [else (string->symbol (format "~a~a" var-prefix (find-best-number nums)))])))
+  (define var-str (symbol->string var))
+  (define var-prefix
+    (let ([m (regexp-match #rx"^(.*[^0-9])[0-9]+$" var-str)])
+      (if m
+          (cadr m)
+          var-str)))
+  (define found-exact-var? #f)
+  (define nums
+    (let loop ([sexp sexp]
+               [nums (set)])
+      (cond
+        [(pair? sexp) (loop (cdr sexp) (loop (car sexp) nums))]
+        [(symbol? sexp) 
+         (when (equal? sexp var)
+           (set! found-exact-var? #t))
+         (define str (symbol->string sexp))
+         (define match (regexp-match #rx"([0-9]+)$" str))
+         (if (and match
+                  (is-prefix? var-prefix str))
+             (set-add nums (string->number (list-ref match 1)))
+             nums)]
+        [else nums])))
+  (cond
+    [(not found-exact-var?) var]
+    [(set-empty? nums) (string->symbol (format "~a1" var))]
+    [else (string->symbol (format "~a~a" var-prefix (find-best-number nums)))]))
 
 (define (find-best-number nums)
-  (let loop ([sorted (sort nums <)]
+  (let loop ([sorted (sort (set->list nums) <)]
              [i 1])
     (cond
       [(null? sorted) i]
       [else 
-       (let ([fst (car sorted)])
-         (cond
-           [(< i fst) i]
-           [(> i fst) (loop (cdr sorted) i)]
-           [(= i fst) (loop (cdr sorted) (+ i 1))]))])))
+       (define fst (car sorted))
+       (cond
+         [(< i fst) i]
+         [(> i fst) (loop (cdr sorted) i)]
+         [(= i fst) (loop (cdr sorted) (+ i 1))])])))
 
 (define (variables-not-in sexp vars)
   (let loop ([vars vars]
@@ -46,14 +48,16 @@
     (cond
       [(null? vars) null]
       [else 
-       (let ([new-var (variable-not-in sexp (car vars))])
-         (cons new-var
-               (loop (cdr vars)
-                     (cons new-var sexp))))])))
+       (define new-var (variable-not-in sexp (car vars)))
+       (cons new-var
+             (loop (cdr vars)
+                   (cons new-var sexp)))])))
 
 (define (is-prefix? str1 str2)
   (and (<= (string-length str1) (string-length str2))
-       (equal? str1 (substring str2 0 (string-length str1)))))
+       (for/and ([c1 (in-string str1)]
+                 [c2 (in-string str2)])
+         (equal? c1 c2))))
 
 (provide/contract
  [variable-not-in (any/c symbol? . -> . symbol?)]
diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/tl-test.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/tl-test.rkt
index 7571b117d5..8aaa5913bf 100644
--- a/pkgs/redex-pkgs/redex-test/redex/tests/tl-test.rkt
+++ b/pkgs/redex-pkgs/redex-test/redex/tests/tl-test.rkt
@@ -2820,6 +2820,7 @@
         (term x4))
   (test (variable-not-in (term (x x1 x1 x2 x2)) 'x)
         (term x3))
+  (test (variable-not-in (term (|| |1|)) '||) '|2|)
   
   (test (variables-not-in (term (x y z)) '(x))
         '(x1))