diff -r e3732ed89dfc -r dd26fbdee924 Quot/Examples/FSet3.thy
--- a/Quot/Examples/FSet3.thy	Fri Jan 08 10:44:30 2010 +0100
+++ b/Quot/Examples/FSet3.thy	Fri Jan 08 11:20:12 2010 +0100
@@ -354,10 +354,17 @@
   shows "fconcat (finsert x S) = x |\<union>| fconcat S"
 apply(lifting concat2)
 apply(injection)
+(* The Relation is wrong to apply rep_abs_rsp *)
+thm rep_abs_rsp[of "(op \<approx> ===> op =)"]
 defer
+apply (simp only: finsert_def[simplified id_simps])
+apply (simp only: fconcat_def[simplified id_simps])
 apply(cleaning)
+(* finsert_def doesn't get folded, since rep-abs types are incorrect *)
 apply(simp add: comp_def)
-apply(cleaning)
+apply (simp add: fconcat_def[simplified id_simps])
+apply cleaning
+(* The Relation is wrong again. *)
 sorry
 
 text {* raw section *}