On 4 Apr 2012, at 14:33, Makarius wrote: > On Wed, 4 Apr 2012, Rob Arthan wrote: > >> >> On 4 Apr 2012, at 11:48, David Matthews wrote: >> >>> On 03/04/2012 16:20, Rob Arthan wrote: >>>> On 30 Mar 2012, at 12:52, David Matthews wrote: >>>> >>>>> Looking carefully at the syntax, though, "op" is not allowed in a >>>>> datatype specification although in all other respects the syntax of >>>>> a binding and a specification are the same. I've added an error >>>>> message if "op" is used in a specification. >>>> >>>> I didn't look at the syntax of modules. You are quite right. In fact, >>>> as far as I can see, op is not allowed anywhere in a signature. >>> >>> I've now reduced the error message to a warning since it seems Isabelle has >>> "op" in signatures. >> >> Tut, tut :-). Somewhat to my surprise, the ProofPower source does comply >> with the standard syntax, even though I was completely unaware that "op" >> wasn't allowed in signatures. > > Historically, we've always tried to minimize the problems in the grey areas > of the SML standard, with its occasional changes that were not immediately > clear from outside. > > I have no problems to remove inappropriate "op" occurrences from the Isabelle > sources, if it does not break SML/NJ or old versions of Poly/ML (5.2.1, > 5.3.0, 5.4.x). On the other hand it will make testing of old Isabelle > versions with brand new Poly/ML versions more difficult. >
I should explain that "Tut, tut" was just intended to be a light-hearted jibe at the Isabelle code. I didn't intend to suggest that Poly/ML should stop supporting the extended syntax that allows your old code to compile. Regards, Rob. _______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
