[isabelle-dev] Inventing names (Re: Bug: Possible generalization error in 'Tactic.rule_by_tactic')

[Alexander Krauss]

Hi Brian,

Brian Huffman wrote:
> I'm sure that many of the internal proofs performed by fixrec and the
> domain package use free variable names like "P" or "x". Without
> locales or local theories, this was never a problem: The global
> context might mention Const "P", but never Free "P". However, local
> theory contexts *can* refer to free variables, and tools need to be
> aware of this.

Yes. Whenever you invent names, you must do this relative to a context.
Also, if you call other tools, you must make sure that the names you 
invented are again known to the context. This corresponds to a "fix" 
command in Isar.

> My question is this: With local theory contexts, what is the right way
> to obtain free variable names that are safe to use in local proofs?

I think the easiest way is to use Variable.variant_fixes.

Alex