1. Fixed get-accessor-range-type-pred to get the correct domain and predicate
   when subtypes are involved
2. In collect-common-accessors, included the constructor in the entries
   (needed for supporting 1.)
Fixed unit-derecognize to return expr if *adt* is set, rather than nil
1. Fixed instantiate-resolution to keep adding new information to the resolution,
   rather than starting over with each new theory instance.
2. Fixed instantiate-operator-type to remove the decl-formals of the current
   declaration from the bindings
1. Fixed subst-mod-params* :around to be more careful about what is put in the
   hash tables
2. In subst-mod-params* (resolution), removed the "res5" assertion
Added type-constraints* (funtype) courtesy of Basile Clement and Simon Halfon
Modified xt-theory-formal to check that parameter is a formal-type-decl and
produce an error if not.
Modified pp* (const-decl) to use :miser instead of :fill
Modified set-type* :around (application) to check the macro for TCCs before
applying it.
Modified generate-assuming-tccs to ensure it is generated for existence-tccs
when in the prover.
1. Modified pvs2cl-constant to call pvs2cl-lisp-function if lisp-function
   returns nil
2. Modified pvs2cl-constructor to set in-name even if eval-info is there
   (somehow eval-info can get set without in-name getting set).
Merged changes