Re: [isabelle] unhelpful comment in Term.ML

On Wed, 11 Nov 2015, Lawrence Paulson wrote:

As the author of both the code and the comment, I can confirm that I always preferred to call this function with singleton lists.

That is why I have called it old-fashioned: in present-day Isabelle, the canonical operations take only a single argument, and are then used with "fold" or "fold_rev" for iteration. There is in fact the one-argument Term.subst_bound as well, although its signature is old-style and requires an older fold combinator.

The reason why these ancient and important term operations have not been reformed significantly, is that they are ancient and important. Certain critical operations depend on them. Too much ambition is likely to cause problems.

When they are touched again, one question would be if the (raise Same.SAME) performance tuning is still relevant. The current Poly/ML runtime system might cope without, but it requires serious empirical studies.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.