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