--- a/Quot/Examples/IntEx.thy	Thu Jan 21 10:55:09 2010 +0100
+++ b/Quot/Examples/IntEx.thy	Thu Jan 21 11:11:22 2010 +0100
@@ -195,9 +195,6 @@
 apply injection
 apply (rule quot_respect(9))
 apply (rule Quotient_my_int)
-
-apply(cleaning)
-apply (simp add: ex1_prs[OF Quotient_my_int])
 done
 
 lemma ho_tst: "foldl my_plus x [] = x"