[isabelle-dev] AFP entry Grith_Chromatic fails with "THM 0"
bulwahn at in.tum.de
Wed Oct 10 18:00:57 CEST 2012
It is probably due to my latest changeset in the
On 10/10/2012 03:50 PM, 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:
> ?'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
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev