--- a/Quot/quotient_term.ML	Thu Feb 04 18:09:20 2010 +0100
+++ b/Quot/quotient_term.ML	Fri Feb 05 10:32:21 2010 +0100
@@ -389,7 +389,6 @@
 val mk_babs = Const (@{const_name Babs}, dummyT)
 val mk_ball = Const (@{const_name Ball}, dummyT)
 val mk_bex  = Const (@{const_name Bex}, dummyT)
-val mk_bex1 = Const (@{const_name Bex1}, dummyT)
 val mk_bex1_rel = Const (@{const_name Bex1_rel}, dummyT)
 val mk_resp = Const (@{const_name Respects}, dummyT)
 
@@ -474,6 +473,24 @@
          else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
+  | (Const (@{const_name "Ex1"}, ty) $ 
+      (Abs (n, _,
+        (Const (@{const_name "op &"}, _) $ 
+          (Const (@{const_name "op :"}, _) $ _ $ (Const (@{const_name "Respects"}, _) $ resrel)) $ 
+          (t $ _)
+        )
+      )), Const (@{const_name "Ex1"}, ty') $ t') =>
+       let
+         val t = incr_boundvars (~1) t
+         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
+         val _ = tracing "bla"
+       in
+         if resrel <> needrel
+         then term_mismatch "regularize (Bex1)" ctxt resrel needrel
+         else mk_bex1_rel $ 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')
@@ -514,17 +531,6 @@
          else mk_bex1_rel $ 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 = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
-       in
-         if resrel <> needrel
-         then term_mismatch "regularize (Bex1)" ctxt resrel needrel
-         else mk_bex1_rel $ resrel $ subtrm
-       end
-
   | (* equalities need to be replaced by appropriate equivalence relations *) 
     (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
          if ty = ty' then rtrm