the simplification rules returned from TFL are now paired with the row they came from.

* Isar/Pure: local results and corresponding term bindings are now subject to Hindley-Milner polymorphism (similar to ML); this accommodates incremental type-inference nicely; * Isar/Pure: new calculational elements 'moreover' and 'ultimately' support plain accumulation of results, without applying any rules yet;

support Hindley-Milner polymorphisms in results and bindings;