>> "A conversion is any function that maps a term t to a theorem |-t==u."
>> LCP, 1983

>> up to beta-equivalence. Since conversions are low-level proof methods which
>> are sensitive to the precise term structure, this is a wart that causes
>> non-modularity. This non-modularity only shows up (to refine Brian's analysis)
>> if the lhs of the rewrite rule has a free variable F in an applied position: F
>> t. This does not happen very often, but if it does, rewr_conv should still
>> behave nicely. It should do a non-normalizing instantiation followed by a
>> beta-normalization.

> Alternatively one could do the normalization before on the input term.
> Empirically, higher-order matching can produce surprises if applied to terms
> with beta redexes, it normally is never used like that in the existing tools.
> So it is better not to give non-normal stuff to the match operation.

> Again, I don't expect too many fundamental problems in this rather small
> incident, but one has to approach it with the proper mindset about how the
> Isabelle code base (and its history) works.

> (Next time I will tell a story how an efficient and fully verified merge-sort
> function included in the core sources caused several days of worries.)

>     Makarius