# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264511327 -3600
# Node ID 0aaeea9255f34eea518bf3812dd835701cb4b32a
# Parent  624af16bb6e4546429d54e713dc26342cd813ee9
Simpler statement that has the problem.

diff -r 624af16bb6e4 -r 0aaeea9255f3 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Jan 26 13:58:28 2010 +0100
+++ b/Quot/Examples/FSet.thy	Tue Jan 26 14:08:47 2010 +0100
@@ -407,12 +407,12 @@
 apply (lifting test4)
 sorry
 
-lemma test5: "\<forall> (x :: 'a list \<Rightarrow> 'a list, y, z) \<in> Respects(
-  prod_rel (op \<approx> ===> op \<approx>) (prod_rel (op \<approx> ===> op \<approx>) (op \<approx> ===> op \<approx>))
-). x = y \<and> y = z"
+lemma test5: "\<forall> (x :: 'a list \<Rightarrow> 'a list, y) \<in> Respects(
+  prod_rel (op \<approx> ===> op \<approx>) (op \<approx> ===> op \<approx>)
+). x = y"
 sorry
 
-lemma "All (\<lambda> (x :: 'a fset \<Rightarrow> 'a fset, y, z). x = y \<and> y = z)"
+lemma "All (\<lambda> (x :: 'a fset \<Rightarrow> 'a fset, y). x = y)"
 apply (lifting test5)
 sorry