[isabelle-dev] Bug: Possible generalization error in 'Tactic.rule_by_tactic'

[Makarius]

On Fri, 9 Apr 2010, 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".

Using completely free variables was causing problems even in the very old 
times.  We have a collection of Isabelle jokes that most people don't 
remember now, such as "datatype foo = a" or "record r = xxx :: nat", or 
the freeze_thaw_robust function.

With the local context you have the chance to get it really right for the 
first time, although that basic functionality to maintain locally fixed 
variables was introduced around 1998 already.


 	Makarius