slight code generator cleanup

removed 'primitive definitions' added (non)strict generation, minor fixes

fixed typo

* Theory syntax: some popular names (e.g. "class", "if") are now keywords. * Isar: schematic goals are no longer restricted to higher-order patterns. * ML/Pure: Logic.(un)varify only works in a global context, which is now enforced.

Schematic invocation of locale expression in proof context.

added invoke.ML;