--- a/Quot/quotient_term.ML	Wed Jan 27 08:41:42 2010 +0100
+++ b/Quot/quotient_term.ML	Wed Jan 27 11:31:16 2010 +0100
@@ -436,6 +436,22 @@
          else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
+  | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
+       let
+         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+       in
+         if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm
+         else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
+       end
+
+  | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
+       let
+         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+       in
+         if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm
+         else mk_bexeq $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
+       end
+
   | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, 
      Const (@{const_name "All"}, ty') $ t') =>
        let
@@ -447,13 +463,6 @@
          else mk_ball $ (mk_resp $ resrel) $ subtrm
        end
 
-  | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
-       let
-         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
-       in
-         if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm
-         else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
-       end
 
   | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, 
      Const (@{const_name "Ex"}, ty') $ t') =>
@@ -466,14 +475,6 @@
          else mk_bex $ (mk_resp $ resrel) $ subtrm
        end
 
-  | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
-       let
-         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
-       in
-         if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm
-         else mk_bexeq $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
-       end
-
   | (Const (@{const_name "Bexeq"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
        let
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')