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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
