--- a/Quot/Examples/FSet.thy	Tue Jan 26 13:38:42 2010 +0100
+++ b/Quot/Examples/FSet.thy	Tue Jan 26 13:53:56 2010 +0100
@@ -391,4 +391,11 @@
 apply(lifting test2)
 done
 
+lemma test3: "All (\<lambda> (x :: 'a list, y, z). x = y \<and> y = z)"
+sorry
+
+lemma "All (\<lambda> (x :: 'a fset, y, z). x = y \<and> y = z)"
+apply(lifting test3)
+done
+
 end