Added code from J pertaining to convert-type-set-to-term.  Quoting
from a comment there, explaining a certain optimization:

; We commented out this case for Version_3.5 because of a soundness issue that
; no longer exists (because we don't create type-prescription rules for
; subversive functions; see putprop-type-prescription-lst).  We left it
; commented out because we thought it was an unimportant case that hasn't been
; missed.  But, while working with Version_6.4, we encountered a proof in a
; script from Warren Hunt that sped up from 77 seconds to 16 seconds when
; including this case.  That script generated a lot of forced assumptions, and
; this code is responsible for creating the clauses proved in the forcing
; round.  In particular, if a lemma is forced in a context in which one of the
; governing assumptions is (< alpha beta), then that assumption is encoded as
; (equal (< alpha beta) t) in the clause attacked by the forcing round -- if
; those clauses are generated by the code in Version_3.5 through Version_6.4,
; i.e., if flg=nil.  But that means the inequality is hidden until the EQUAL is
; rewritten, delaying, for example, tau.  In the Hunt script, tau can prove
; the clauses generated with flg = t.  So, as of Version_6.5 we restored this
; case, conditional on flg.

Added mod suggested by Jared that allows *default-hs* (the default
hons-space) to be nil not only for ACL2(p), but in general, which can
support possible ttags-based applications.

Fixed a couple of comment typos pointed out by D. Rager.


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1316 5d84a466-a78b-0930-a311-59b22171a541
Made a slight efficiency improvement to hons-equal.  Thanks to Jared
for taking a look at this and encouraging me to make the change.


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1317 5d84a466-a78b-0930-a311-59b22171a541