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

Johannes Hölzl hoelzl at in.tum.de
Wed Oct 10 15:50:21 CEST 2012


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:
  ?'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

When I write 

  using card_left_less_pair[of A] assms by simp

it works.

 - Johannes

More information about the isabelle-dev mailing list