[isabelle-dev] AFP entry Grith_Chromatic fails with "THM 0"

[Makarius]

On Wed, 10 Oct 2012, Johannes Hölzl wrote:

> I tried to build AFP/Grith_Chormatic, but the simplifier fails in
>
>  Ugraphs.thy line 168:
>
>    using card_left_less_pair assms by simp
>
>
> with the following exception:
>
>  exception THM 0 raised (line 790 of "drule.ML"):
>  Ill-typed instantiation:
>  Type
>  ?'a ⇒ ?'b
>  of variable ?f
>  cannot be unified with type
>  (?'a × ?'a) set ⇒ bool of
>  term finite
>  ?x = ?y ⟹ ?f ?x = ?f ?y

It was still OK with Isabelle/28e37eab4e6f and AFP/77f79b2076f1, so I 
guess it is related to the update of the set_comprehension_pointfree 
simproc that emerged in the meantime.


 	Makarius