On Wed, 10 Feb 2016, David Matthews wrote:
fun f x y = x+y; that will fall back to the default "int". Also, all the library functions that use "int" e.g. Array.sub, String.size, List.length or TextIO.inputN, will still have the fixed precision int.
This reminds me of the situation in SML/NJ, before I spent some efforts to force int = IntInf.int on it. It includes a somewhat "patched" basis library like this: http://isabelle.in.tum.de/repos/isabelle/file/9343649abb09/src/Pure/RAW/prop...
I'm inclined to think that having a "configure" option would be the answer.
That would greatly simplify the Isabelle setup, because we always provide a separately compiled version of Poly/ML.
Since we are about to discontinue SML/NJ altogether, it would allow to remove the above tricks, and not move them over to Poly/ML.
Makarius