[isabelle-dev] Variable "?n" has two distinct types

[Makarius]

On Sun, 6 Feb 2011, Gerwin Klein wrote:

> I've managed to get the following error message with Isabelle2011 when 
> running simp:
>
> *** exception TYPE raised (line 109 of "envir.ML"): Variable "?n" has 
> two distinct types *** At command "apply" (line 14 of 
> "/Users/kleing/Simp.thy")
>
> The end of the simplifier trace shows this rule being produced, which 
> indeed has "?n" with different types:
>
> [1]Procedure "defined EX" produced rewrite rule: \<exists>x. ?n (?p S) = 
> Some x \<and> ?n S = x \<equiv> \<exists>x. ?n S = x \<and> ?n (?p S) = 
> Some x

Quick inspection of the sources + history reveals abc655166d61 "now works 
for schematic terms as well".

Before that change, the global context ProofContext.init_global thy was 
sufficient for the Goal.prove due to absence of local operations.  With 
Variable.import_terms and Variable.export one needs to take the context 
seriously, i.e. pass it through the Quantifier1 tool suite as explicit 
argument, which should be a trivial exercise in "localization".

BTW, the naming convention "global" indicates that one needs to watch out 
for problems with lack of context (this is now made explicit in the Isar 
implementation manual).


 	Makarius