diff -r de9e5faf1f03 -r 46cc6708c3b3 Quot/quotient_term.ML
--- 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