--- a/Quot/Examples/SigmaEx.thy	Tue Jan 26 11:13:08 2010 +0100
+++ b/Quot/Examples/SigmaEx.thy	Tue Jan 26 12:06:47 2010 +0100
@@ -113,12 +113,8 @@
 translations
   "\<exists>\<exists> x. P"   == "Ex (%x. P)"
 
-lemma split_rsp[quot_respect]: 
-  "((R1 ===> R2 ===> op =) ===> (prod_rel R1 R2) ===> op =) split split"
-by auto
-
 lemma rvar_rsp[quot_respect]: "(op = ===> alpha_obj) rVar rVar"
-by (simp add: a1)
+  by (simp add: a1)
 
 lemma robj_rsp[quot_respect]: "(list_rel (prod_rel op = alpha_method) ===> alpha_obj) rObj rObj"
 sorry
@@ -150,7 +146,9 @@
 apply (simp)
 prefer 2
 apply cleaning
-apply simp
+apply (subst ex_prs)
+apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
+apply (rule refl)
 sorry
 
 lemma tolift':