--- 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