[isabelle-dev] Conversions between ('a * 'a) set and 'a => 'a => bool relations

[Stefan Berghofer]

Florian Haftmann wrote:
> * This is mainly a question to Stefan: there are some theorems commented
> out (e.g. »thm sym_INTER [to_pred]«) on which pred_set_conv chokes.  I
> guess this is due to a higher-order situation, but I would be reassuring
> if you can confirm that.

Hi Florian,

this looks like a bug. The culprit seems to be function mk_to_pred_inst in
inductive_set.ML, which does not handle variables of type "... => T set"
properly. A similar problem might also occur with to_set. I'll try to fix
this before the next release.

Greetings,
Stefan