diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
index 6eb25d59..e4491bbc 100644
--- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
@@ -91,7 +91,7 @@
 
 (define-syntax (tc-e/t stx)
   (syntax-parse stx
-    [(_ e t) (syntax/loc stx (tc-e e #:ret (ret t (-FS (list) (list (make-Bot))))))]))
+    [(_ e t) (syntax/loc stx (tc-e e #:ret (ret t (-FS -top -bot))))]))
 
 ;; duplication of the mzscheme toplevel expander, necessary for expanding the rhs of defines
 ;; note that this ability is never used
diff --git a/collects/typed-scheme/typecheck/tc-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss
index 9be99d9b..5eef5691 100644
--- a/collects/typed-scheme/typecheck/tc-metafunctions.ss
+++ b/collects/typed-scheme/typecheck/tc-metafunctions.ss
@@ -10,12 +10,6 @@
          unstable/debug
          (for-syntax scheme/base))
 
-;(provide (all-defined-out))
-
-(define-syntax-rule (d/c/p (name . args) c . body)
-  (begin (d/c (name . args) c . body)
-         (p/c [name c])))
-
 ;; this implements the sequence invariant described on the first page relating to Bot
 
 (define (combine l1 l2)
diff --git a/collects/typed-scheme/typecheck/tc-subst.ss b/collects/typed-scheme/typecheck/tc-subst.ss
index a1ddb45b..0613dda2 100644
--- a/collects/typed-scheme/typecheck/tc-subst.ss
+++ b/collects/typed-scheme/typecheck/tc-subst.ss
@@ -12,10 +12,6 @@
 
 ;(provide (all-defined-out))
 
-(define-syntax-rule (d/c/p (name . args) c . body)
-  (begin (d/c (name . args) c . body)
-         (p/c [name c])))
-
 (d/c/p (open-Result r objs ts)
        (-> Result? (listof Object?) (listof Type/c) (values Type/c FilterSet? Object?))
        (match r
@@ -27,12 +23,13 @@
                     (subst-filter-set fs k o #t arg-ty)
                     (subst-object old-obj k o #t)))]))
 
-(d/c/p (subst-filter-set fs k o polarity t)
-       (-> FilterSet? name-ref/c Object? boolean? Type/c FilterSet?)
+(d/c/p (subst-filter-set fs k o polarity [t #f])
+       (->* (FilterSet? name-ref/c Object? boolean?) ((or/c #f Type/c)) FilterSet?)
+       (define extra-filter (if t (make-TypeFilter t null k) -top))
   (match fs
     [(FilterSet: f+ f-)
-     (combine (subst-filter (-and (make-TypeFilter t null k) f+) k o polarity)
-	      (subst-filter (-and (make-TypeFilter t null k) f-) k o polarity))]))
+     (combine (subst-filter (-and extra-filter f+) k o polarity)
+	      (subst-filter (-and extra-filter f-) k o polarity))]))
 
 (d/c/p (subst-type t k o polarity)
      (-> Type/c name-ref/c Object? boolean? Type/c)
diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss
index 10d77c7f..06de85c3 100644
--- a/collects/typed-scheme/types/abbrev.ss
+++ b/collects/typed-scheme/types/abbrev.ss
@@ -14,7 +14,7 @@
          (for-syntax scheme/base syntax/parse)
 	 (for-template scheme/base scheme/contract scheme/promise scheme/tcp scheme/flonum))
 
-(provide (all-defined-out)
+(provide (except-out (all-defined-out) -FS)
          (rename-out [make-Listof -lst]))
 
 ;; convenient constructors
@@ -120,7 +120,7 @@
 (define -no-obj (make-Empty))
 
 
-(d/c (-FS + -)
+(d/c/p (-FS + -)
      (c:-> Filter/c Filter/c FilterSet?)
      (match* (+ -)
              [((Bot:) _) (make-FilterSet -bot -top)]
diff --git a/collects/typed-scheme/types/convenience.ss b/collects/typed-scheme/types/convenience.ss
deleted file mode 100644
index 8619e113..00000000
--- a/collects/typed-scheme/types/convenience.ss
+++ /dev/null
@@ -1,73 +0,0 @@
-#lang scheme/base  
-(require "../utils/utils.ss"
-         (rep type-rep filter-rep object-rep rep-utils)
-         (utils tc-utils)
-         "abbrev.ss" (only-in scheme/contract current-blame-format)
-	 (types comparison printer union subtype utils)
-         scheme/list scheme/match scheme/promise
-         (for-syntax syntax/parse scheme/base)
-         unstable/debug syntax/id-table scheme/dict
-         scheme/trace
-         (for-template scheme/base))
-
-(provide (all-defined-out)
-         (all-from-out "abbrev.ss")
-         ;; these should all eventually go away
-         make-Name make-ValuesDots make-Function
-         (rep-out filter-rep object-rep))
-
-(define (one-of/c . args)
-  (apply Un (map -val args)))
-
-(define (Un/eff . args)
-  (apply Un (map tc-result-t args)))
-
-
-;; if t is of the form (Pair t* (Pair t* ... (Listof t*)))
-;; return t*
-;; otherwise, return t
-;; generalize : Type -> Type
-(define (generalize t)
-  (let/ec exit
-    (let loop ([t* t])
-      (match t*
-        [(Value: '()) (-lst Univ)]
-	[(Value: 0) -Nat]
-        [(Mu: var (Union: (list (Value: '()) (Pair: _ (F: var))))) t*]
-        [(Pair: t1 (Value: '())) (-lst t1)]
-        [(Pair: t1 t2)
-         (let ([t-new (loop t2)])
-           (if (type-equal? (-lst t1) t-new)
-               t-new
-               (exit t)))]
-        [_ (exit t)]))))
-
-
-;; DO NOT USE if t contains #f
-(define (-opt t) (Un (-val #f) t))
-
-(define In-Syntax
-  (-mu e
-       (*Un (-val null) -Boolean -Symbol -String -Keyword -Char -Number 
-            (make-Vector (-Syntax e))
-            (make-Box (-Syntax e))
-            (-lst (-Syntax e))
-            (-pair (-Syntax e) (-Syntax e)))))
-
-(define Any-Syntax (-Syntax In-Syntax))
-
-(define (-Sexpof t)
-  (-mu sexp
-       (Un (-val '())
-           -Number -Boolean -Symbol -String -Keyword -Char           
-           (-pair sexp sexp)
-           (make-Vector sexp)
-           (make-Box sexp)
-           t)))
-
-(define -Sexp (-Sexpof (Un)))
-
-(define Syntax-Sexp (-Sexpof Any-Syntax))
-
-(define Ident (-Syntax -Symbol))
-
diff --git a/collects/typed-scheme/utils/utils.ss b/collects/typed-scheme/utils/utils.ss
index 4b52d5ab..376bc954 100644
--- a/collects/typed-scheme/utils/utils.ss
+++ b/collects/typed-scheme/utils/utils.ss
@@ -162,7 +162,11 @@ at least theoretically.
 
 ;; turn contracts on and off - off by default for performance.
 (define-for-syntax enable-contracts? #t)
-(provide (for-syntax enable-contracts?) p/c w/c cnt d-s/c d/c)
+(provide (for-syntax enable-contracts?) p/c w/c cnt d-s/c d/c d/c/p)
+
+(define-syntax-rule (d/c/p (name . args) c . body)
+  (begin (d/c (name . args) c . body)
+         (p/c [name c])))
 
 ;; these are versions of the contract forms conditionalized by `enable-contracts?'
 (define-syntax p/c