--- a/Quot/Examples/FSet.thy	Tue Dec 08 15:12:55 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 08 15:42:29 2009 +0100
@@ -437,9 +437,7 @@
 defer
 apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
-thm lambda_prs[OF identity_quotient Quotient_fset]
-thm lambda_prs[OF identity_quotient Quotient_fset, simplified]
-apply(simp only: lambda_prs[OF identity_quotient Quotient_fset,simplified])
+apply(tactic {* clean_tac @{context} 1 *}) (* TODO: needs lambda_prs twice *)
 sorry
 
 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))"