[isabelle] Confusing behavior of a paired set comprehension

the following definition is interpreted in a confusing way:

def ident :: "'a set => ('a \times 'a) set"
where "ident S = {(x,x) . x \in S}"

the command "thm ident_def" yields
ident ?S \<equiv> {(xa, x). x \<in> ?S}

Should this be considered as a bug?


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