# [isabelle] TERM exception in fologic.ML

Back in October 2014 I reported an error that I encountered when updating IsarMathLib to Isabelle 2014.The error is still there in Isabelle2016-RC1. This can be replicated by checking the following theory (in Isabelle/ZF logic):
theory Scratch imports func
begin
lemma func_imagedef: assumes A1: "f:X\<rightarrow>Y" and A2: "A\<subseteq>X"
Â shows "f``(A) = {f`(x). x \<in> A}"
proof
Â from A1 show "f``(A) \<subseteq> {f`(x). x \<in> A}"
ÂÂÂ using image_iff apply_iff by auto
Â show "{f`(x). x \<in> A} \<subseteq> f``(A)"
Â proof
ÂÂÂ fix y assume "y \<in> {f`(x). x \<in> A}"
ÂÂÂ then obtain x where "x\<in>A \<and> y = f`(x)"
ÂÂÂÂÂ by auto
ÂÂÂ with A1 A2 show "y \<in> f``(A)"
ÂÂÂÂÂ using apply_iff image_iff by auto
Â qed
qed
end
which givesÂ
exception TERM raised (line 47 of "~~/src/FOL/fologic.ML"):
Â dest_Trueprop
Â âf A B.
ÂÂÂÂ âa b. f â Pi(A, B) â
ÂÂÂÂÂÂÂÂÂÂ âa, bâ â f â a â A â f ` a = b
in Isabelle/jEdit tooltip at the last auto keyword.
This is not a very important problem for me as I can work around it, but maybe it's good to know that it is still there.
Slawomir Kolodynski

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*