On 23/01/17 12:25, Lawrence Paulson wrote:
> I’m not sure what to conclude from this. It’s about non-functional
> behaviour, so not quite something people ought to rely upon.
> I’m guessing one could make the change and nothing would happen. I’m
> still not convinced that the case for a change has been made however.
>> On 22 Jan 2017, at 08:18, Florian Haftmann
>> <mailto:florian.haftm...@informatik.tu-muenchen.de>> wrote:
>> Surprisingly (?), there is no error here. The reason is obvious when
>> inspecting src/Pure/library.ML:
>> ML ‹
>> fun (f oo g) x y = f (g x y);
>> fun (f ooo g) x y z = f (g x y z);
>> fun (f oooo g) x y z w = f (g x y z w);
Such a subtle change of semantics would also require a change of the
name, otherwise we get into a mire of unclear meaning of Isabelle/ML
sources over a long history.
In this case there is not even a clear indication to go this way or that
way with partial application: making it more strict can cause other
Also note that oo, ooo, oooo are relatively old-fashioned and rarely
used these days.
isabelle-dev mailing list