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

[Johannes Hölzl]

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