David Matthews is working on a new release of Poly/ML in which the default type
of integers is fixed-precision. A configuration option can restore the former
set up, but that might be a mistake: I modified MetiTarski to use large
integers only where needed and saw runtime decrease by around 30%. We could do
the same. I imagine that we need large integers almost nowhere. Now consider
that every bound variable is represented internally by an integer.
isabelle-dev mailing list