[isabelle-dev] AFP entry Grith_Chromatic fails with "THM 0"
Makarius
makarius at sketis.net
Wed Oct 10 17:08:25 CEST 2012
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
More information about the isabelle-dev
mailing list