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 >> <florian.haftm...@informatik.tu-muenchen.de >> <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 surprises. Also note that oo, ooo, oooo are relatively old-fashioned and rarely used these days. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev