[isabelle] TERM exception in fologic.ML

When I was updating the IsarMathLib project for Isabelle 2014 I got the following:
*** exception TERM raised (line 47 of "~~/src/FOL/fologic.ML"):
*** dest_Trueprop
*** !!f A B. ALL a b. f : Pi(A, B) --> <a, b> : f <-> a : A & f ` a = b
*** At command "by" (line 605 of "~/Projects/IsarMathLib/isarmathlib-1.9.1/IsarMathLib/func1.thy")
*** exception TERM raised (line 47 of "~~/src/FOL/fologic.ML"):
*** dest_Trueprop
*** !!a A B. a : Sigma(A, B) --> <fst(a), snd(a)> = a
*** At command "by" (line 296 of "~/Projects/IsarMathLib/isarmathlib-1.9.1/IsarMathLib/Topology_ZF_10.thy")

I was able to work around this by rewriting the proofs slightly. I understand that the TERM exceptions are not just failures to check a proof but some internal errors (?), so I just wanted to report this for consideration for the next release.
The exception can be replicated by checking the following theory (in ZF logic)
theory Scratch imports func


lemma func_imagedef: assumes A1: "f:X\<rightarrow>Y" and A2: "A\<subseteq>X"
  shows "f``(A) = {f`(x). x \<in> A}"
  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)"
    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


Regards,,Slawomir Kolodynski http://savannah.nongnu.org/projects/isarmathlib
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)

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