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

[Lukas Bulwahn]

It is probably due to my latest changeset in the 
set_comprehension_pointfree simproc.

Lukas

On 10/10/2012 03:50 PM, Johannes Hölzl wrote:
> Hi,
>
> 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
>
> There is no instantiation happening in the Isar text.
>
> Isabelle hg: 9a2a53be24a2, afp hg: 2b6348e4bda7, near the current tips.
>
> It seems to happen somewhere internal when instantiating
> card_left_less_pair.
>
> When I write
>
>    using card_left_less_pair[of A] assms by simp
>
> it works.
>
>   - Johannes
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev