[isabelle-dev] Problem with transfer method

[Brian Huffman]

On Mon, Sep 30, 2013 at 2:34 PM, Makarius <makarius at sketis.net> wrote:
> According to the normal context discipline, free variables are always fixed,
> like a local const.  We have a few tools that violate that principle and
> consequently cause confusion, e.g. the Simplifier. There are sometimes
> historical reasons for that, and little hope for reforms.
>
> Is this also the case for transfer?

If you're asking whether transfer distinguishes the term constructors
Free and Const, then the answer is yes. Transfer may generalize a Free
(according to the heuristic) but will never generalize over a Const.

With more and more localized tools using Frees as constants, perhaps
it would be more robust for transfer to treat Free and Const exactly
the same. I will have to think more about this.

- Brian