Modified non-recursive-constructor to take subtypes into account
Fixed minor errors
Added str as quick unparse
1. Added library to mk-modname calls in add-usings-to-context*
   (recursive-type)
2. Modified adt? (type-name) and constructors (type-name) to restore
   the adt slot if it is a symbol (this can happen after loading bin files)
3. Added assertion to create-formulas* and create-definition-formula
Changed calls to "chmod" to "/bin/chmod" - required by recent change to SBCL,
added to others to be more secure.

Provided by Jerry James
Fix for pvs-sxhash-bits for SBCL from Jerry James
1. Modified get-current-imported-theories to be able to get library recursive
   types, which are not otherwise available.
2. Fixed get-adt-slot-value to try harder to get a library adt

These should fix a bug reported by Cesar Munoz 2013-02-20
1. Modified generate-adt-predicate and gen-adt-reduce-selection to generate
   the uncurried forms for codatatypes.
2. Fixed gen-adt-reduce-bindings** to generate dependent bindings correctly
Added mapped-eq-def-tcc class
Modified subtype-of*? (adt-type-name subtype) to make it more robust in
getting the adt slot properly set after restoring from bin files.
Added free-params-acts and free-params-dacts as the free parameter computation
is not quite the same for these two cases.
Added mk-mapped-eq-def-tcc
Added :char-width nil to str definition
Modified ext-find-recognizer-subtype (adt-type-name subtype) to make it more
robust in getting the adt slot properly set after restoring from bin files.
Modified resolve-theory-actuals to take dactuals into account
1. Modified type-expr-from-print-type (type-name) to include the decl in call
   to subst-mod-params
2. Modified type-expr-from-print-type (type-application) to set the
   current-declaration during the restore
1. Modified set-type-mapping-rhs to allow defined constants
2. Modified instantiate-sel-resolution to make it more robust in
   getting the adt slot properly set after restoring from bin files.
3. Fixed conditions on assertion in instantiate-operator-type
4. Fixed bindings-to-modinsts to only get the associated-decl for
   decl-formal-types
5. Fixed set-type* (if-expr) to bind iftype to the type if the compatible-type
   is a dep-binding
6. Modified set-type* (type-name) to work correctly during a restore from
   binfile
Added some hack to check if Emacs on Mac has been configured for X
Added this hack for Mac Emacs