[isabelle-dev] a problem with interpretations in FinFun

[Ondřej Kunčar]

This refers to 68c163598f07 + my local patches in Lifting/Transfer.

During testing my local patches, I found out that I broke the theory 
FinFun.thy

In every interpretation I got an error message "Illegal free variables 
in expression: ...". For example for the first interpretation, it was 
"b'". I don't think the error was related to my local changes since I 
didn't change anything in locales and even if I did something strange 
with contexts in lift_definition, it should be ok when we are back at 
the toplevel.

I "fixed" the problem by writing "for b'" (for g and so on) for each 
interpretation. But funnily after I restarted Jedit, I cannot reproduce 
this problem any more, i.e, FinFun goes through even without these "for 
b'" additional statements.

Another strange thing that might or might not be related: when I
hovered over b' in this expression

interpretation finfun_update: comp_fun_commute "λa f. f(a :: 'a $:= b')"

I got originally(=in the state with the error message mentioned above) 
this type:
free variable
:: 'b
But now I get this:
free variable
:: 'b
:: 'b
(i.e., 'b is there twice)

Since I cannot reproduce this problem any more, might be hard to say 
anything about it, but maybe it rings a bell in somebody's head.

Ondrej