[isabelle-dev] A possible bug with Isabelle 2013

[Makarius]

On Fri, 1 Mar 2013, Lawrence Paulson wrote:

> In Edinburgh LCF, term quotations containing anonymous type variables 
> were simply rejected. Perhaps that would still be the best approach now. 
> I'm not convinced that it would lead to more errors than the 'a itself 
> approach.

I know, you've explained that to me many years ago.

For us now, it means to mark-up these critical spots where polymoprhism 
emerges.  The information can then be somehow visualized for the user. 
It is also possible to get a systematic overview over all reachable 
Isabelle applications (including AFP) how things actually happens in the 
wild.

The latter is not just for empirical exploration of sources.  With formal 
markup of certain kind over the text, that can be "refactored" 
systematically.  I am here not so much thinking of eliminating legitimate 
uses of polymorphism, but things like cleaning up notation to avoid the 
mix of --> and ⟶ symbols.


 	Makarius