More useful error message when someone tries mkExpr(VARIABLE).
Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (resolves bug #548).