[isabelle] Misleading tooltips on Isabelle-Terms with coercions in isabelle/jedit


when giving the semantics tutorial this morning, I ran into quite
strange tooltips in Isabelle/jedit: Consider, 

theory Scratch
imports Complex_Main

term "∃a::nat. ∃b::real. a+b=0"

when hovering over the a in "a+b" and pressing Ctrl, I get the following
  bound "a"
  bound variable
  :: real

This tooltip is simply wrong! The variable a still has type nat. So I
would have expected either a::nat, or "real a :: real".


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