--- a/Quot/Examples/SigmaEx.thy	Thu Jan 28 10:52:10 2010 +0100
+++ b/Quot/Examples/SigmaEx.thy	Thu Jan 28 12:24:49 2010 +0100
@@ -128,8 +128,8 @@
 sorry
 
   
-lemma bex1_bex1reg: "(\<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_bex1reg: "(\<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)
@@ -207,10 +207,10 @@
  \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =).
  \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =).
 
- Bexeq (alpha_obj ===> op =) (\<lambda>hom_o\<Colon>robj \<Rightarrow> 'a .
- Bexeq (list_rel (prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b.
- Bexeq ((prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c.
- Bexeq (alpha_method ===> op =) (\<lambda>hom_m\<Colon>rmethod \<Rightarrow> 'd.
+ Bex1_rel (alpha_obj ===> op =) (\<lambda>hom_o\<Colon>robj \<Rightarrow> 'a .
+ Bex1_rel (list_rel (prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b.
+ Bex1_rel ((prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c.
+ Bex1_rel (alpha_method ===> op =) (\<lambda>hom_m\<Colon>rmethod \<Rightarrow> 'd.
 (
  (\<forall>x. hom_o (rVar x) = fvar x) \<and>
  (\<forall>d. hom_o (rObj d) = fobj (hom_d d) d) \<and>