--- a/Quot/QuotBase.thy	Thu Jan 28 10:52:10 2010 +0100
+++ b/Quot/QuotBase.thy	Thu Jan 28 12:24:49 2010 +0100
@@ -451,19 +451,19 @@
   using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply
   by metis
 
-section {* Bexeq quantifier *}
+section {* Bex1_rel quantifier *}
 
 definition
-  Bexeq :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+  Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
 where
-  "Bexeq R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))"
+  "Bex1_rel R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))"
 
 (* TODO/FIXME: simplify the repetitions in this proof *)
 lemma bexeq_rsp:
   assumes a: "Quotient R absf repf"
-  shows "((R ===> op =) ===> op =) (Bexeq R) (Bexeq R)"
+  shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)"
 apply simp
-unfolding Bexeq_def
+unfolding Bex1_rel_def
 apply rule
 apply rule
 apply rule
@@ -500,9 +500,9 @@
 
 lemma ex1_prs:
   assumes a: "Quotient R absf repf"
-  shows "((absf ---> id) ---> id) (Bexeq R) f = Ex1 f"
+  shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f"
 apply simp
-apply (subst Bexeq_def)
+apply (subst Bex1_rel_def)
 apply (subst Bex_def)
 apply (subst Ex1_def)
 apply simp
@@ -535,8 +535,8 @@
 apply metis
 done
 
-lemma bex1_bexeq_reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bexeq R (\<lambda>x. P x))"
-  apply (simp add: Bex1_def Ex1_def Bexeq_def in_respects)
+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 clarify
   apply auto
   apply (rule bexI)