diff -r 0b29650e3fd8 -r d8f07b5bcfae Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Dec 08 22:26:01 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 08 23:30:47 2009 +0100
@@ -435,6 +435,9 @@
 apply(simp)
 apply(rule allI)
 apply(rule list_eq_refl)
+apply(cleaning)
+apply(simp add: fun_map.simps expand_fun_eq)
+apply(cleaning)
 done
 
 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))"
@@ -462,4 +465,7 @@
 apply(tactic {* lambda_prs_tac @{context} 1 *})
 (* Until here is ok *)
 apply(cleaning)
+sorry
+
+
 end