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_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
