--- 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,