--- a/Quot/Examples/SigmaEx.thy	Tue Jan 26 15:59:04 2010 +0100
+++ b/Quot/Examples/SigmaEx.thy	Tue Jan 26 16:30:51 2010 +0100
@@ -85,14 +85,14 @@
  \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =).
  \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =).
 
- Bexeq
-   (prod_rel (alpha_obj ===> op =)
+ Bex1
+   (Respects (prod_rel (alpha_obj ===> op =)
      (prod_rel (list_rel (prod_rel (op =) alpha_method) ===> op =)
        (prod_rel ((prod_rel (op =) alpha_method) ===> op =)
          (alpha_method ===> op =)
        )
      )
-   )
+   ))
 (\<lambda> (hom_o\<Colon>robj \<Rightarrow> 'a, hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b, hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c, hom_m\<Colon>rmethod \<Rightarrow> 'd).
 
 
@@ -128,6 +128,16 @@
 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)
+apply clarify
+apply auto
+apply (rule bexI)
+apply assumption
+apply (simp add: in_respects)
+apply (simp add: in_respects)
+apply auto
+done
 
 lemma liftd: "
 Ex1 (\<lambda>(hom_o, hom_d, hom_e, hom_m).

--- a/Quot/QuotBase.thy	Tue Jan 26 15:59:04 2010 +0100
+++ b/Quot/QuotBase.thy	Tue Jan 26 16:30:51 2010 +0100
@@ -535,6 +535,17 @@
 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)
+  apply clarify
+  apply auto
+  apply (rule bexI)
+  apply assumption
+  apply (simp add: in_respects)
+  apply (simp add: in_respects)
+  apply auto
+  done
+
 section {* Various respects and preserve lemmas *}
 
 lemma quot_rel_rsp:

--- a/Quot/quotient_tacs.ML	Tue Jan 26 15:59:04 2010 +0100
+++ b/Quot/quotient_tacs.ML	Tue Jan 26 16:30:51 2010 +0100
@@ -132,7 +132,7 @@
   0. preliminary simplification step according to
      ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range
 
-  1. eliminating simple Ball/Bex instances (ball_reg_right bex_reg_left)
+  1. eliminating simple Ball/Bex/Bex1 instances (ball_reg_right bex_reg_left)
 
   2. monos
 
@@ -159,7 +159,7 @@
 in
   simp_tac simpset THEN'
   REPEAT_ALL_NEW (CHANGED o FIRST' 
-    [resolve_tac @{thms ball_reg_right bex_reg_left},
+    [resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg},
      resolve_tac (Inductive.get_monos ctxt),
      resolve_tac @{thms ball_all_comm bex_ex_comm},
      resolve_tac eq_eqvs,  

--- a/Quot/quotient_term.ML	Tue Jan 26 15:59:04 2010 +0100
+++ b/Quot/quotient_term.ML	Tue Jan 26 16:30:51 2010 +0100
@@ -476,6 +476,16 @@
          val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty'))
        in
          if resrel <> needrel
+         then term_mismatch "regularize(bex1_res)" ctxt resrel needrel
+         else mk_bexeq $ resrel $ subtrm
+       end
+
+  | (Const (@{const_name "Bex1"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
+       let
+         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+         val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty'))
+       in
+         if resrel <> needrel
          then term_mismatch "regularize(bex1)" ctxt resrel needrel
          else mk_bexeq $ resrel $ subtrm
        end