diff --git a/collects/typed-scheme/env/lexical-env.ss b/collects/typed-scheme/env/lexical-env.ss
index 04ddc7a9..9998ad3c 100644
--- a/collects/typed-scheme/env/lexical-env.ss
+++ b/collects/typed-scheme/env/lexical-env.ss
@@ -23,8 +23,8 @@
 
 ;; find the type of identifier i, looking first in the lexical env, then in the top-level env
 ;; identifer -> Type
-(define (lookup-type/lexical i)
-  (lookup (lexical-env) i 
+(define (lookup-type/lexical i [env (lexical-env)])
+  (lookup env i 
           (lambda (i) (lookup-type 
                        i (lambda () 
                            (cond [(lookup (dotted-env) i (lambda _ #f))
@@ -35,7 +35,7 @@
 
 ;; refine the type of i in the lexical env
 ;; (identifier type -> type) identifier -> environment
-(define (update-type/lexical f i)
+(define (update-type/lexical f i [env (lexical-env)])
   ;; do the updating on the given env
   ;; (identifier type -> type) identifier environment -> environment
   (define (update f k env)
@@ -48,9 +48,9 @@
   ;; check if i is ever the target of a set!
   (if (is-var-mutated? i)
       ;; if it is, we do nothing
-      (lexical-env)
+      env
       ;; otherwise, refine the type
-      (update f i (lexical-env))))
+      (update f i env)))
 
 ;; convenience macro for typechecking in the context of an updated env
 (define-syntax with-update-type/lexical
diff --git a/collects/typed-scheme/env/type-environments.ss b/collects/typed-scheme/env/type-environments.ss
index 8095c806..57c04ee6 100644
--- a/collects/typed-scheme/env/type-environments.ss
+++ b/collects/typed-scheme/env/type-environments.ss
@@ -2,12 +2,14 @@
 
 (provide current-tvars
          extend
+         env?
          lookup
          make-empty-env
          extend-env
          extend/values
          dotted-env
          initial-tvar-env
+         env-map
          with-dotted-env/extend)
 
 (require (prefix-in r: "../utils/utils.ss"))
@@ -29,7 +31,8 @@
 ;; the environment for types of ... variables
 (define dotted-env (make-parameter (make-empty-env free-identifier=?)))
 
-
+(define (env-map f env)
+  (make-env (env-eq? env) (map f (env-l env))))
 
 ;; extend that works on single arguments
 (define (extend e k v) 
diff --git a/collects/typed-scheme/typecheck/tc-envops.ss b/collects/typed-scheme/typecheck/tc-envops.ss
index ba631895..2b4f8496 100644
--- a/collects/typed-scheme/typecheck/tc-envops.ss
+++ b/collects/typed-scheme/typecheck/tc-envops.ss
@@ -1,12 +1,13 @@
 #lang scheme/base
 
 (require (rename-in "../utils/utils.ss" [infer infer-in]))
-(require (rename-in (types subtype convenience remove-intersect)                   
+(require (rename-in (types subtype convenience remove-intersect union)                   
                     [-> -->]
                     [->* -->*]
                     [one-of/c -one-of/c])
          (infer-in infer)
          (rep type-rep)
+         (only-in (env type-environments lexical-env) env? update-type/lexical env-map)
          scheme/contract scheme/match
          stxclass/util
          (for-syntax scheme/base))
@@ -42,3 +43,11 @@
      (restrict t u)]
     [(t (NotTypeFilter: u (list) _))
      (remove t u)]))
+
+(define/contract (env+ env fs)
+  (env? (listof Filter/c) . -> . env?)
+  (for/fold ([Γ env]) ([f fs])
+    (match f
+      [(Bot:) (env-map (lambda (_) (Un)) Γ)]
+      [(or (TypeFilter: _ _ x) (NotTypeFilter: _ _ x))
+       (update-type/lexical (lambda (x t) (update t f)) x Γ)])))