Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-04-03 19:29:56 -0700 (Sun, 03 Apr 2005)
Revision: 7105
Log message:
Removed the $ignore check in input term checking. I had forgotten
that the check is not being used on declarations.
It brings up another issue: input checking is not being
used on terms that are being declared (because the term doesn't
exist yet). However, it is probably a good idea to do input
checking on all the subterms.
The other place where the input checker is bypassed is for
iforms, and in the !!!WARNING!!! section of Term_grammar. We
should probably add checking where appropriate.