--- a/Quot/QuotBase.thy	Thu Feb 04 18:09:20 2010 +0100
+++ b/Quot/QuotBase.thy	Fri Feb 05 10:32:21 2010 +0100
@@ -434,9 +434,9 @@
 
 lemma bex1_rsp:
   assumes a: "(R ===> (op =)) f g"
-  shows "(Bex1 (Respects R) f = Bex1 (Respects R) g)"
+  shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)"
   using a 
-by (simp add: Ex1_def Bex1_def in_respects) auto
+by (simp add: Ex1_def in_respects) auto
 
 (* 3 lemmas needed for cleaning of quantifiers *)
 lemma all_prs:
@@ -536,7 +536,7 @@
 done
 
 lemma bex1_bexeq_reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
-  apply (simp add: Bex1_def Ex1_def Bex1_rel_def in_respects)
+  apply (simp add: Ex1_def Bex1_rel_def in_respects)
   apply clarify
   apply auto
   apply (rule bexI)