--- a/Quot/Examples/SigmaEx.thy	Tue Jan 26 12:24:23 2010 +0100
+++ b/Quot/Examples/SigmaEx.thy	Tue Jan 26 13:38:42 2010 +0100
@@ -144,11 +144,6 @@
 apply (lifting tolift)
 apply (regularize)
 apply (simp)
-prefer 2
-apply cleaning
-apply (subst ex_prs)
-apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
-apply (rule refl)
 sorry
 
 lemma tolift':