[isabelle-dev] adhoc overloading: order inserting overloaded constant

[Makarius]

On Sat, 1 Feb 2014, Christian Sternagel wrote:

> So my idea was to instead use top-down rewriting (i.e., first replace 
> maximal subterms that fit a given pattern). This is what 
> "Pattern.rewrite_term_top" does, right? So after replacing 
> "rewrite_term" by "rewrite_term_top", I get the expected results.
>
> Now my question. Can anybody think of a reason why "rewrite_term_top" 
> would not be generally preferable over "rewrite_term" inside of 
> "insert_overloaded"?

This is an old story.  Printing usually works better top-down, e.g. see 
good old 'translations' with their yo-yo strategy.  When 'abbreviation' 
was introduced, there was Pattern.rewrite_term, but not 
Pattern.rewrite_term_top yet, so there was no other way.

I kept telling Stefan Berghofer about that omission until he made an 
laternative version in 2010: see 6e45e4c94751, 5d2fe4e09354 (with typical 
tell-nothing log entries).

So in analogy, the same will probably work for adhoc_overloading as well, 
without going through all the reasoning again.


> If not, could one of the devs incorporate this tiny change please?

OK, I will try this out.


 	Makarius